Skip to main content
43 votes

Proof assistants for beginners - a comparison

Lean I am a professional mathematician with minimal experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into ...
Kevin Buzzard's user avatar
40 votes

Proof assistants for beginners - a comparison

Coq The easiest proof assistant to start with is The assistant with the best learning resources The assistant with a great community The assistant with the nicest libraries in that order of priority....
Agnishom Chattopadhyay's user avatar
22 votes

Proof assistants for beginners - a comparison

I believe it will depend a lot on your experience and sensibility, but that a good way of getting started is to have a look at lets-prove-leftpad : This is a repository of provably-correct versions ...
Clément's user avatar
  • 321
18 votes
Accepted

Tools for checking the consistency of a type theory

One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A ...
Andrej Bauer's user avatar
  • 9,792
18 votes
Accepted

What is the difference between refl and rfl in Lean 3?

So you are correct that refl is a tactic, and rfl is a term, so for example: ...
It'sNotALie.'s user avatar
  • 1,445
16 votes

Proof assistants for beginners - a comparison

I'll answer the question "What is the easiest proof assistant to start with for a programmer" and take the sub-questions one-by-one. Which one is the easiest to pick as a language? Agda, ...
Max Heiber's user avatar
16 votes

Proof assistants for beginners - a comparison

(This answer was originally for another question, but others thought it was better as an answer for this question, or for this question.) I think for these sorts of questions it depends a lot on your ...
Jason Rute's user avatar
  • 9,160
15 votes

Proof assistants for beginners - a comparison

The Incredible Proof Machine There is no need to learn syntax to enter, you just drag and drop boxes and connect them, and still learn a lot about rigorous proofs, intro and elim rules, local ...
Joachim Breitner's user avatar
13 votes
Accepted

Explanation of Coq math-comp repositories

As Meven wrote, the Mathematical Components repositories originate from the work of Georges Gonthier and his team proving first the Four Color Theorem, then the Odd Order Theorem. In Coq people do not ...
Zimm i48's user avatar
  • 637
13 votes
Accepted

What is the current state of proof assistants?

These are broad questions and I doubt you will get a complete answer in a single stack exchange answer. But since you seem ernest and interested, let me at least try to help clarify some of your ...
Jason Rute's user avatar
  • 9,160
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

Proof assistants for beginners - a comparison

The part of your answer I like best is a "Python of proof assistants". :) When I see "Python" I read "a programming language which is deceptively simple on the surface level ...
Alex Chichigin's user avatar
11 votes

Strong induction on ℕ with function α → ℕ

Here's how to prove Andrej Bauer's corrected statement using the induction tactic: ...
Eric's user avatar
  • 971
11 votes

Explanation of Coq math-comp repositories

Roughly, Mathematical Components are a set of libraries that are designed to work together, and follow a lot of common ideas and guidelines, in particular the use of the SSReflect proof language, ...
Meven Lennon-Bertrand's user avatar
10 votes

Formalizations of unsolved problems

The closest to what you are asking for might be the Formal abstracts project whose aim is to formalize the statements (but no proofs) of results from papers. Formalizing statements without proofs is ...
Andrej Bauer's user avatar
  • 9,792
10 votes
Accepted

How to replace a function by its body

The tactic you are looking for is probably unfold. If you write unfold bexp it will replace it with its body. In certain cases, ...
Théo Winterhalter's user avatar
9 votes

Proof assistants for beginners - a comparison

The main issue with this question is that it asks to compare proof assistants on several points but people who answer cannot know enough about all proof assistants to make this comparison point by ...
9 votes

What is the difference between refl and rfl in Lean 3?

Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between ...
Eric's user avatar
  • 971
9 votes
Accepted

Strong induction on ℕ with function α → ℕ

...
Andrej Bauer's user avatar
  • 9,792
9 votes
Accepted

How to define curry in Lean

If Lean checks your code you know it is correct. (Well, that and the fact there is only one curry function up to functional equivalence.) Now as for how to use ...
Jason Rute's user avatar
  • 9,160
8 votes

How do I express a negative premise in Coq?

This is not a Coq issue. Rather, Coq rightfully complains that a relation such as the one you envision might not be well-defined. Indeed, suppose you had another (perfectly valid) premise ...
Meven Lennon-Bertrand's user avatar
8 votes

Why is $\Bbb Z = \Bbb N$ independent of Lean?

It suffices to give two models of Lean's type theory, one in which $\mathbb{Z} = \mathbb{N}$ and another in which $\mathbb{Z} \ne \mathbb{N}$. We shall use the interpretation of Lean type theory in ...
Andrej Bauer's user avatar
  • 9,792
8 votes
Accepted

Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

Follow the structure of the function you are proving things about. Looking at the definition of Ascii.eqb (shown below), it is defined using ...
Li-yao Xia's user avatar
  • 2,032
7 votes
Accepted

How do you import part of the standard library in Coq?

The recommended import to get the many lemmas associated with nat is Require Import Arith. This includes ...
Li-yao Xia's user avatar
  • 2,032
7 votes
Accepted

What mathematical topics should I learn first before I start using proof assistants?

I came to proof assistants from TCS about a year ago, so perhaps I am well placed to answer your question. This may be somewhat opinion-based, but I don't feel it is necessary to learn category theory ...
Bolton Bailey's user avatar
7 votes

Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...
Joey Eremondi's user avatar
7 votes
Accepted

Coq defining a hierarchy of collections of integers with infinitely many "levels"

A simple way is to define the type in terms of the Peano natural numbers nat. ...
Bubbler's user avatar
  • 684
7 votes

Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

I mean, it's still exhaustive case analysis, but intros [[] [] [] [] [] [] [] []]; reflexivity. at least is shorter. If you use ...
djao's user avatar
  • 609
6 votes

What mathematical topics should I learn first before I start using proof assistants?

I would say the most confusing (and often frustrating) notion for many first users is that types are not sets, so unless you plan on using a proof assistant specifically based on set theory (almost ...
Couchy's user avatar
  • 2,300
6 votes
Accepted

How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

The exercise gives starting instructions: intro h rw [<- is_zero_suc a] These give the following proof state: ...
James Wood's user avatar
  • 1,053

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