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
1 answer
79 views

Well founded recursion through lists

2 votes
1 answer
30 views

What is the precise meaning of "reducible"?

2 votes
1 answer
106 views

Rewriting with heterogeneous equality (JMeq)

6 votes
2 answers
231 views

Lean4 Exercise: Double negation implies law of excluded middle

21 votes
1 answer
383 views

What is the difference between `leanprover` and `leanprover-community` GitHub repositories?

2 votes
1 answer
284 views

Lean 4 Importing into VSCode

2 votes
0 answers
67 views

How does Lean `simp` tactic work?

2 votes
0 answers
34 views

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

1 vote
1 answer
81 views

Lean: what does the syntax `variable [ring R]` mean?

1 vote
2 answers
117 views

Dependent sum and equality with Coq

2 votes
1 answer
139 views

(Dis)Advantages of basing a proof assistant on CH correspondence?

2 votes
1 answer
31 views

How to prove across language boundaries about functions written in another language via FFI?

2 votes
1 answer
77 views

How to prove a statement about sublists?

3 votes
1 answer
247 views

Does lean 4 have built-in dictionary types?

Browse more Questions