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

6 votes
2 answers
110 views

Why are impredicative constructions used less in type theory than in material set theory?

44 votes
2 answers
895 views

Are some proof assistants better suited for given areas of math than others?

20 votes
1 answer
261 views

Examples of formalisation of abelian categories

23 votes
2 answers
481 views

Why haven't all of the "hundred greatest theorems" been formalized yet?

14 votes
4 answers
274 views

Algorithms obtained through constructive formalization

16 votes
1 answer
504 views

Proof assistants and formalised mathematics in the MSC database

22 votes
3 answers
320 views

To what extent is formalized mathematics publishable?

28 votes
2 answers
717 views

What set-theoretic definitions can't easily be formalized in a type theory?

19 votes
1 answer
294 views

How hard is computing integrals in Lean?

8 votes
1 answer
112 views

Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?

8 votes
1 answer
109 views

What are some useful resources for a mathematician interested in learning Isabelle/HOL?

13 votes
2 answers
144 views

verifying combinatorial constructions - choice of a proof assistant

17 votes
2 answers
174 views

How can I prove facts about floating point calculations?

11 votes
2 answers
108 views

Proof assistants with dynamic scope/local instances/etc.?

Browse more Questions