Skip to main content
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 ...
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.
13 votes

What are good books for learning about proof assistants for Functional Analysis?

In the Coq wiki, you'll find a list of books and tutorials which are great resources. I personally recommend the Software foundations course (started by B. Pierce, but with many contributors over the ...
cbl's user avatar
  • 139
12 votes

What are good books for learning about proof assistants for Functional Analysis?

I personally found the book Mathematical Components by Assia Mahboubi and Enrico Tassi to be the best resource for learning about Coq.
Neil Strickland's user avatar
12 votes

What are good examples of April fools jokes in the proving assistant community?

I don't know if Falso itself was "released" on April 1st, but an implementation of it Isabelle/HOLF was. Of course, this is a very powerful proof assistant and it is a shame that an ...
Andrew Marmaduke'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", ...
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
Accepted

What are good books for learning about proof assistants for Functional Analysis?

The question could be summed up as a request for resources about formalizing functional analysis in proof assistants. For this, I would recommend: Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia ...
Alex Nelson's user avatar
  • 1,564
11 votes
Accepted

What are the possible kinds of type theories or logics with quotients?

If I may advertise me and my coauthor's own work, our paper Observational Equality : Now for Good describes $\mathrm{TT}^{\mathrm{obs}}$, a relatively simple dependent type theory that is a variation ...
Loïc Pujet's user avatar
  • 1,469
10 votes

What are good examples of April fools jokes in the proving assistant community?

Brunhilde/Rhein 2015, as announced on the Isabelle mailing list was a fully working German translation of Isabelle/HOL, including keywords. It also came with a homepage, example documents and ...
Joachim Breitner's user avatar
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 ...
10 votes

What are good books for learning about proof assistants for Functional Analysis?

This a bit of a roundabout suggestion, but Avigad's excellent Foundations article summarizes the variety of logics that are used to build proof assistants. EDIT: I decided to update the post with ...
Pedro Sánchez Terraf's user avatar
10 votes

What are good books for learning about proof assistants for Functional Analysis?

For Isabelle/HOL there is the book Concrete Semantics (pdf) by Tobias Nipkow and Gerwin Klein which is a great introduction but it also covers a great deal more than just an introduction would: Part ...
Wno-all's user avatar
  • 1,108
9 votes

What are good books for learning about proof assistants for Functional Analysis?

Handbook of Practical Logic and Automated Reasoning (Site) (WorldCat) (Code and resources) HOL Light was written by John Harrison (ref) who also authored "Handbook of Practical Logic and ...
Guy Coder's user avatar
  • 2,846
9 votes

What are good books for learning about proof assistants for Functional Analysis?

For Agda you can try Verified Functional Programming in Agda by Aaron Stump. Its first part is a rather good introduction to the language, somewhat similar to Software Foundations.
Andrei Halanay's user avatar
9 votes
Accepted

How to implement a visual proof assistant?

Your question is pretty broad. How would I implement and reason about a graphical calculus or proof assistant? First (almost tautologically) I think you need to carefully consider two questions: ...
Jason Rute's user avatar
  • 8,665
8 votes

Formal description of algorithmic subtyping/cumulativity

See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.
Andrej Bauer's user avatar
  • 9,144
8 votes

What are the possible kinds of type theories or logics with quotients?

I do not have specific suggestions for what type theories with quotients one might look at, but I would like to explain what sort of obstacle one faces when designing a proof assistant with quotients. ...
Andrej Bauer's user avatar
  • 9,144
8 votes

What are good examples of April fools jokes in the proving assistant community?

Metamath has a list of April fool theorems. An excerpt of the explanations: To derive avril1, we have used an interdisciplinary approach that combines concepts ...
7 votes
Accepted

PDEs and proof assistants

Have you seen the updates from more recent work of the same Coq group you cite? To quote from their article this week: Our long-term purpose is to formally prove the correctness of parts of a library ...
macbeth's user avatar
  • 394
7 votes

PDEs and proof assistants

A fragment of traditional PDE theory has been formalized in Mizar: Sora Otsuki and Pauline N. Kawamoto and Hiroshi Yamazaki, "A Simple Example for Linear Partial Differential Equations and Its ...
Alex Nelson's user avatar
  • 1,564
7 votes

Mechanization of game semantics?

A student of mine has a partial formalization of game semantics for affine logic based on "A game semantics for linear logic" by Andreas Blass. The winning strategies for more complicated ...
Jason Gross's user avatar
  • 1,537
6 votes
Accepted

Parameterized Datatypes in a Universe à la Tarski?

Arg : (c : Code) -> (El c -> Desc) -> Desc Are you sure this is what you mean? I think the usual constructor is closer to the following: ...
gallais's user avatar
  • 1,126
6 votes

What are good books for learning about proof assistants for Functional Analysis?

A basic introduction is the book ML for the Working Programmer by L. C. Paulson. It is a programming book for the Standard ML language, yet it covers all the basics of functional programming, and ...
tinlyx's user avatar
  • 2,034
5 votes
Accepted

Formal description of algorithmic subtyping/cumulativity

For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ...
Meven Lennon-Bertrand's user avatar
5 votes

Mechanization of game semantics?

Maybe this answer is not quite in the spirit of your question, however the work "CryptHOL: Game-Based Proofs in Higher-Order Logic" (ref) and its implementation on AFP (ref) provide a ...
Wno-all's user avatar
  • 1,108
5 votes

How to implement a visual proof assistant?

A graphical proof assistant for higher categories under active development is homotopy.io, which follows the tradition of Globular. The underlying notion of higher structure used by homotopy.io is ...
Maximilian Doré's user avatar

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