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"?

21 votes
1 answer
383 views

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

2 votes
0 answers
67 views

How does Lean `simp` tactic work?

1 vote
1 answer
81 views

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

2 votes
1 answer
139 views

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

1 vote
0 answers
76 views

Lean proofs for graph algorithms

3 votes
1 answer
100 views

Programming challenge site for lean4

1 vote
1 answer
103 views

Prove an upper bound on the computation time of the Euclidean algorithm in lean4

23 votes
1 answer
502 views

How to search for an existing theorem in Lean?

2 votes
4 answers
1k views

Can we prove every provable statement with Lean?

0 votes
1 answer
93 views

increasing the universe level of a type in Lean by force

1 vote
1 answer
76 views

Type of Sets with an Assocaitive Operation in Lean

0 votes
1 answer
59 views

Minimizing proof environment change while proving in Lean

Browse more Questions