40 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
39 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
  • 8,969
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
  • 8,495
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
  • 627
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
  • 8,495
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
  • 8,969
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
  • 8,969
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
  • 8,495
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
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
  • 1,727
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
  • 674
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,211
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
5 votes
Accepted

How to implement first-order relational structures in Coq?

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as ...
Andrej Bauer's user avatar
  • 8,969
5 votes
Accepted

Referencing previous fields when constructing new structure

There isn't, and I don't think it would be a good idea to change that because it could easily lead to unintentional shadowing. The only language I know that has recursive record instantiation, Nix, ...
Sebastian Ullrich's user avatar
5 votes
Accepted

Proof Review: Basic theorem about ternary relations in Coq

I decided to formalize this in Coq in the simplest way possible, defining a new type $T * T * T \to 2$ In proof assistants and functional programming languages more generally, it's generally more ...
Jason Gross's user avatar
  • 1,457

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