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

39 votes
2 answers
708 views

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

20 votes
1 answer
245 views

Examples of formalisation of abelian categories

24 votes
2 answers
421 views

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

14 votes
4 answers
261 views

Algorithms obtained through constructive formalization

16 votes
1 answer
491 views

Proof assistants and formalised mathematics in the MSC database

22 votes
3 answers
298 views

To what extent is formalized mathematics publishable?

27 votes
2 answers
597 views

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

18 votes
1 answer
252 views

How hard is computing integrals in Lean?

7 votes
1 answer
106 views

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

7 votes
1 answer
90 views

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

11 votes
2 answers
127 views

verifying combinatorial constructions - choice of a proof assistant

17 votes
2 answers
158 views

How can I prove facts about floating point calculations?

11 votes
2 answers
106 views

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

9 votes
1 answer
102 views

Representing $\Bbb RP^2$ in Lean: building a type representing a particular set

Browse more Questions