Questions tagged [tutorials]

Use this tag when looking for tutorials relating to proof assistants. See also [learning].

Filter by
Sorted by
Tagged with
4 votes
1 answer

Tutorial implementation of analytic tableaux

I am re-reading John Harrison's wonderful Handbook of Practical Logic and Automated Reasoning, and he has a rather idiosyncratic presentation of analytic tableaux. What other tutorial implementations ...
  • 1,429
7 votes
0 answers

Tutorial implementations of extensional type theories

There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
  • 3,063
14 votes
4 answers

What games are there?

A game is a fun interactive tutorial/puzzle/challenge that provides the user with a DAG of definitions, theorem statements, examples, etc. and asks the user to prove all the theorems in this DAG. For ...
21 votes
1 answer

Tutorials for formalizing mathematical definitions/statements in Lean

tl;dr: Are there any good introductions/tutorials on how to formalize definitions and theorem statements in Lean? (in contrast to introductions on formalizing proofs) Some background: I am a phd ...
  • 441
13 votes
2 answers

Finding symbols in Lean

There was already a question here of this type but I would like to ask more generally: If I see some strange unicode symbols being used in Lean, is there a recommended way to find out how to type them,...
38 votes
7 answers

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

Many programming language tutorials start with a simple program which just outputs "Hello, World!" to the console or another output. For the various proof assistants, is there some widely-...