Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

0 votes
0 answers
3 views

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

3 votes
1 answer
52 views

Auxiliary Typeclasses in Lean

2 votes
1 answer
40 views

How do we know that we can trust proof assistance to produce correct results?

2 votes
1 answer
26 views

Debug autorewrite in Coq

0 votes
1 answer
22 views

inherit_doc attribute Lean 4

2 votes
3 answers
140 views

How to prove the termination of Ackermann in Lean?

0 votes
2 answers
86 views

How to prove basic lemmas about divisibility in Coq?

12 votes
1 answer
547 views

What are the complex induction patterns supported by Agda?

0 votes
1 answer
68 views

Well founded recursion through lists

2 votes
1 answer
55 views

Abstracting over large types in type theory

4 votes
3 answers
96 views

How does Z3 "exhaustively search" real numbers?

2 votes
1 answer
70 views

Rewriting with heterogeneous equality (JMeq)

1 vote
1 answer
39 views

Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?

0 votes
1 answer
83 views

Dependent sum and equality with Coq

Browse more Questions