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 ...
- 1,175
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 ...
- 786
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-...
- 786
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:
...
- 2,330
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 ...
- 1,455
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....
- 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-...
- 502
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 ...
- 4,344
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 &...
- 361
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 ...
- 3,270
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 ...
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:
...
- 704
Only top scored, non community-wiki answers of a minimum length are eligible