# Tag Info

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,165

### 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 ...
• 766
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-...
• 766

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

Defining lists, usually: list A := Nil | Cons of A * list A Defining append for lists: ...
• 2,231

### 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,445
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

### 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-...

### 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 ...

### 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 ...

### 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 ...

### 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 ...
• 3,967

### 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 &...

### 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,070
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 ...