Skip to main content
56 votes
Accepted

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

I think that to a large extent this is an open problem, and I think that one reason it's still open is that not enough people are working on it. I would love to see some change here but right now I ...
Kevin Buzzard's user avatar
30 votes
Accepted

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

Almost no pen-and-paper mathematics is written in ZFC. The vast majority of mathematical texts is actually written in something that resembles structural set theory and is closer to type theory than ...
Andrej Bauer's user avatar
  • 9,802
28 votes

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

The main difficulty in formalising a proof of Fermat's Last Theorem is that all the known human proofs involve a vast amount of algebraic and analytic geometry (thousands of pages) and a vast amount ...
Kevin Buzzard's user avatar
23 votes

Where can I find lists of theorems that have been verified?

The Lean community maintains several of such lists: https://leanprover-community.github.io/undergrad.html keeps track of which part of a French undergrad curriculum have been added to mathlib https://...
21 votes

Where can I find lists of theorems that have been verified?

Freek Wiedijk maintains a list of 100 theorems, and pointers to formalizations in many different systems: https://www.cs.ru.nl/~freek/100/ The 100 theorems on the list were chosen a long time ago (and ...
19 votes

Examples of new mathematics discovered through formalization?

One quite concrete example of this is discussed by Massot in the essay linked in the original post. During the work on the Liquid Tensor Experiment (formalizing the proof of a theorem due to Scholze ...
18 votes

How can I prove facts about floating point calculations?

I recommend the monograph Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System by Sylvie Boldo and Guillaume Melquiond. It addresses your questions and much, ...
Andrej Bauer's user avatar
  • 9,802
18 votes

Where can I find lists of theorems that have been verified?

Mizar publishes them quarterly in their journal Formalized Mathematics.
17 votes

Where can I find lists of theorems that have been verified?

Coq has an official Coq opam repository (see the accompanying Package Index or that of coq.io). These make it easy to search contributed formalization packages and ...
17 votes

Where can I find lists of theorems that have been verified?

Metamath has such an extensive interlinked library. A list of theorems in metamath is available here.
14 votes
Accepted

Proof assistants and formalised mathematics in the MSC database

TL;DR: Based on the descriptions in the MSC2020 alone, I would use the new section 68Vxx, specifically the subject classification 68V20 (or maybe 68V15) if one is formalizing mathematics in a proof ...
Jason Rute's user avatar
  • 9,195
12 votes

To what extent is formalized mathematics publishable?

The ITP and CPP conferences regularly accept papers on mechanised mathematics. See previous programs at, for example: ITP 2016, where there were among others, papers such as A Formal Proof of Cauchy’...
Michael Norrish's user avatar
12 votes

Where can I find lists of theorems that have been verified?

If you're interested in homotopy type theoretical foundations, I took a stab just today at comparing what's in the various HoTT math libraries. It's a list of both theorems and "theories", ...
12 votes
Accepted

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

Regarding natural numbers, and inductive types (ie. initial algebras of some form) in general, impredicative encodings are inconvenient, as they only specify weakly initial algebras, rather than ...
Meven Lennon-Bertrand's user avatar
11 votes

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

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at ...
Mike Shulman's user avatar
  • 3,200
11 votes
Accepted

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

Let me answer your immediate question first with the following code snippet (which relies on mathlib): ...
Adam Topaz's user avatar
11 votes

Where can I find lists of theorems that have been verified?

Most of the main theorem provers have central libraries of formal mathematics. Here I've including their official statistics (accurate as of 2022-02-10) and more importantly a link to where you can ...
11 votes

How hard is computing integrals in Lean?

I'm going to inflate Mario's comment to an answer: You can absolutely write tactics in Lean to do this. What you'll be doing is creating a large part of a CAS, but as a Tactic. This would be largely a ...
Jacques Carette's user avatar
10 votes
Accepted

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

Once you installed Isabelle (following these instructions), you will have all the materials listed on the tag isabelle as a local copy. Definitely go through this one for a good (field agnostic) ...
Wno-all's user avatar
  • 1,128
10 votes

Where can I find lists of theorems that have been verified?

From a similar question asked at cs.stackexchange.com. Note: Only added info not already noted in existing answers. Proofwiki "Mizar Mathematical Library" gigantic library A graph of the ...
7 votes
Accepted

verifying combinatorial constructions - choice of a proof assistant

If I understand you correctly, you will be working with finite discrete objects, such as finite fields, finite groups, finite combinatorial objects, etc. I would recommend using a proof assistant ...
Andrej Bauer's user avatar
  • 9,802
7 votes

What is known about minimal sets of axioms?

From the point of view of the proof assistants, Metamath is an interesting tool for studying minimal sets of axioms. In the set.mm database, classical propositional ...
Thierry Arnoux's user avatar
7 votes

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

"Presumably, each theorem presents its own difficulties." For Fermat's Last Theorem, I agree with the answer by Andrew Wiles' academic grandson and the comments currently on the question. ...
Nike Dattani's user avatar
  • 1,165
6 votes

Examples of new mathematics discovered through formalization?

As David Roberts mentioned in a comment, this happens relatively frequently in the field of homotopy type theory / univalent foundations. Often in that area (at least, in my experience), a proof-...
6 votes

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

I don't think most theorem provers are very different from each other. In my opinion most provers are based around classical logic, intuitionistic logic or possibly linear logic. Many theorem provers ...
Ms. Molly Stewart-Gallus's user avatar
6 votes

Exotic natural language summaries of formal proofs

It is certainly possible to generate summaries of formal proofs that are readable by people familiar only with the standard mathematical vernacular. Some formal proof languages like Naproche, Isar or ...
Slawomir K.'s user avatar
6 votes

To what extent is formalized mathematics publishable?

I don't know if there are well-established rules yet. My guess would be that it depends on how significant the differences are between X and Y. If the mathematics is new, then of course it can be ...
Mike Shulman's user avatar
  • 3,200
6 votes

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

Induction over impredicative encodings requires internalizing a small amount of parametricity. See https://cedille.github.io/ for an example of a language that does this. Otherwise working around the ...
Ms. Molly Stewart-Gallus's user avatar
5 votes

To what extent is formalized mathematics publishable?

I once asked a similar question in the Coq Zulip chat (regular link, no-login-needed link). This was my takeaway: If your formalization is interesting as code, you can publish it from that angle. In ...
Ana Borges's user avatar
5 votes

To what extent is formalized mathematics publishable?

I know I am almost two years late in the game, but a new journal dedicated to publishing articles about formalized mathematics, and aimed at mathematicians rather than computer scientists, has just ...
Filippo Alberto Edoardo's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible