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

5 votes
2 answers
121 views

Unclarity about Preorder class in Lean4

2 votes
1 answer
26 views

How to unfold definitions in Lean / find the right theorems to apply?

1 vote
1 answer
51 views

Question about default definitions in fields

3 votes
2 answers
106 views

Coq: can `tauto` be used to prove classical tautologies?

4 votes
1 answer
87 views

How to prove a property of a conditional statement without using tactics in Lean?

3 votes
0 answers
61 views

Where is the discriminate tactic defined in Coq?

6 votes
1 answer
133 views

What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?

4 votes
1 answer
80 views

Using induction to define Indexed family of HITs in agda

2 votes
1 answer
74 views

Why does my previously defined function expands/computes to itself?

4 votes
2 answers
221 views

Why is my recursive definition of list_min ill-formed?

7 votes
1 answer
367 views

What is the current state of proof assistants?

3 votes
2 answers
165 views

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

8 votes
2 answers
286 views

Strong induction on ℕ with function α → ℕ

5 votes
1 answer
105 views

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

Browse more Questions