Skip to main content
28 votes
Accepted

What's the "Hello, World!" for proof assistants?

The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello ...
Nike Dattani's user avatar
  • 1,165
19 votes

What's the "Hello, World!" for proof assistants?

These might be somewhat advanced for an honest "Hello, world!" but I think that the irrationality of $\sqrt 2$ and the infinitude of primes are two very common get-the-feet-wet projects for ...
jmc's user avatar
  • 766
18 votes
Accepted

Tutorials for formalizing mathematical definitions/statements in Lean

Lean for the Curious Mathematician 2020 You seem to be the exact right audience for this workshop. We have video recordings on youtube: https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-...
jmc's user avatar
  • 766
17 votes

What's the "Hello, World!" for proof assistants?

Defining lists, usually: list A := Nil | Cons of A * list A Defining append for lists: ...
Couchy's user avatar
  • 2,231
16 votes

What's the "Hello, World!" for proof assistants?

Another example could be the definition of natural numbers (for type-theoretic assistants): inductive nat : Type | zero : nat | succ : nat → nat This also shows ...
It'sNotALie.'s user avatar
  • 1,445
16 votes
Accepted

Finding symbols in Lean

Unicode character input is an editor feature, so this answer is specific to VSCode. If you have a Lean file open in VSCode, you can hover over a unicode symbol to see what input commands are available....
Rob Lewis's user avatar
  • 593
14 votes

What's the "Hello, World!" for proof assistants?

A "Hello, World!" of proof assistants should be available in as many languages as possible. As pointed out by Clément in his answer to a different question, there are around twenty provably-...
Bruno Le Floch's user avatar
14 votes

What games are there?

Cubical Agda suggestions The HoTT game The HoTT Game was written by some Imperial undergraduates; the goal is to prove that the fundamental group of the circle is the integers, in cubical Agda. You ...
14 votes

What games are there?

Lean suggestions The max minigame Short online game here. Something I knocked off with a couple of collaborators when we were trying to work out how to make a real number game. We still haven't got to ...
11 votes

What games are there?

The incredible proof machine proof-machine is a game with a collection of theorems for classical propositional logic, classical first-order logic, and the simply typed lambda calculus. Example (think ...
10 votes

What's the "Hello, World!" for proof assistants?

Many proof assistants based on an intensional type theory equipped with inductive types may choose the commutativity (or simpler, associativity) of addition as the "Hello world". This shows ...
Trebor's user avatar
  • 3,967
10 votes

What's the "Hello, World!" for proof assistants?

Proving some elementary results on propositions but using the language of types could be a good option for languages where that makes sense, since it makes clear some of the motivation behind the &...
Sean O'Connor's user avatar
6 votes

Finding symbols in Lean

If you are using Emacs, then the corresponding command is C-u C-x =. This displays a buffer with lots of information about the character under point, including its ...
Mike Shulman's user avatar
  • 3,070
5 votes
Accepted

Tutorial implementation of analytic tableaux

As far as I'm aware, leanTAP was written in just a few lines of Prolog, and it works with first-order formulas in Skolem normal forms. There's a tutorial implementation in OCaml which looks similar to ...
Zhanrong Qiao's user avatar
3 votes

What games are there?

Coq suggestions Çoqoban A sokoban where your solution is a proof. You can play it in your browser thanks to the awesome work of Shachar Itzhaky (one of the jsCoq maintainers): https://coq-next.vercel....
1 vote

What's the "Hello, World!" for proof assistants?

For a "Hello World" for proof assistants I personally use the fact that reversing a list is an involution: ...
Alex Chichigin's user avatar

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