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

8 votes
2 answers
261 views

Strong induction on ℕ with function α → ℕ

4 votes
1 answer
85 views

Looking for an entry point in the universe of proof assistants and proof IDE's

3 votes
1 answer
133 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

4 votes
0 answers
67 views

Display style proofs using Coq

2 votes
1 answer
166 views

Lemma about splitting of homogeneous polynomial equations into irreducible equations

6 votes
2 answers
245 views

Problem proving a binary add function

6 votes
1 answer
184 views

How to replace a function by its body

8 votes
2 answers
650 views

Explanation of Coq math-comp repositories

9 votes
1 answer
488 views

How to define curry in Lean

31 votes
8 answers
906 views

Proof assistants for beginners - a comparison

13 votes
2 answers
173 views

Tools for checking the consistency of a type theory

9 votes
1 answer
155 views

Generating valid statements without a proof goal

16 votes
1 answer
300 views

Formalizations of unsolved problems

9 votes
2 answers
187 views

Comparison between proof assistants for coinductive structures and proofs

Browse more Questions