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
132 views

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
116 views

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
308 views

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
211 views

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
158 views

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
1k views

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