< User:Boris TsirelsonRevision as of 06:16, 9 August 2010 by imported>Boris Tsirelson
For a mathematical theory, correctness means formalizability.
Top 100 theorems in Isabelle +
Formalizing 100 Theorems +
Isabelle +
Download and installation +
Projects +
The Isabelle2009-2 Library +
IsarMathLib: A library of formalized mathematics for Isabelle/ZF
(CC) Image: Boris Tsirelson The graphical user interface started.
The graphical user interface started.
(CC) Image: Boris Tsirelson The source file is read.
The source file is read.
(CC) Image: Boris Tsirelson Definitions are processed; the formulation of the first lemma is being processed.
Definitions are processed; the formulation of the first lemma is being processed.
(CC) Image: Boris Tsirelson The formulation of the first lemma is processed; the goal is pending.
The formulation of the first lemma is processed; the goal is pending.
(CC) Image: Boris Tsirelson At last, a really serious lemma.
(CC) Image: Boris Tsirelson The goal.
(CC) Image: Boris Tsirelson "We have", why?
(CC) Image: Boris Tsirelson Here is why!
(CC) Image: Boris Tsirelson Really complicated arguments...
(CC) Image: Boris Tsirelson Happy end is coming.
(CC) Image: Boris Tsirelson The theorem is proved.
(CC) Image: Boris Tsirelson Some options of the Proof General.
(CC) Image: Boris Tsirelson Isabelle, show us your methods...
(CC) Image: Boris Tsirelson ...and your term bindings...
(CC) Image: Boris Tsirelson ...and the theorems.