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

Is the de Morgan interval Kan?

1 vote
1 answer
28 views

Using the contrapositive in lean 4

8 votes
4 answers
160 views

Are there any ergonomic ways to deal with finite types in Coq?

1 vote
0 answers
63 views

How to reason about equality between different datatypes?

3 votes
3 answers
155 views

Rewrite with definitional equality and dependent types

0 votes
1 answer
46 views

Why doesn't the `div` predicate work here?

0 votes
1 answer
42 views

I don't know how to fire up coqtail

2 votes
1 answer
21 views

Picking this and calculation in Isabelle/JEdit output

8 votes
1 answer
111 views

How "generic" are "generic proof assistants"?

1 vote
1 answer
46 views

How to write a low-level proof in Isar?

0 votes
2 answers
154 views

Make ChatGPT write formal proof from natural language proof

1 vote
1 answer
44 views

unexpected inductive type occurrence error for recursive inductive type

2 votes
2 answers
101 views

How to abstract over function arity in Lean and Coq?

0 votes
1 answer
73 views

an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert

Browse more Questions