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

2 votes
0 answers
48 views

Comparison of normal forms in Normalization by Evaluation

16 votes
2 answers
276 views

What are the advantages to impredicativity?

8 votes
1 answer
174 views

Why is `--irrelevant-projections` unsafe in Agda?

13 votes
0 answers
251 views
+50

Unintentionally proven false theorem with type-in-type outside logic and foundations?

4 votes
1 answer
87 views

Lean4 Exercise: Double negation implies law of excluded middle

2 votes
0 answers
43 views

Cannot open pixbuf loader module file in Windows

7 votes
2 answers
154 views

Figures on computer proof assistant usage

3 votes
2 answers
82 views

Proving with non-structural recursion in Lean4

2 votes
1 answer
81 views

Applying custom tactic in hypothesis

2 votes
0 answers
63 views

Is there a good demonstration of bidirectional type checking with strict Prop?

7 votes
2 answers
2k views

Why are these two proofs so different?

4 votes
3 answers
1k views

Are there computable functions which can't be expressed in Lean?

1 vote
1 answer
140 views

Is type checking in "Ideal Lean" computably enumerable?

5 votes
1 answer
117 views

Explain all the arguments to this rec eliminator

Browse more Questions