User:Boris Tsirelson/Sandbox1

For a mathematical theory, correctness means formalizability. "In practice, the mathematician ... is content to bring the exposition to a point where his experience and mathematical flair tell him that translation into formal language would be no more than an exercise of patience (though doubtless a very tedious one)."

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.

References

Bourbaki, Nicolas (1968), Elements of mathematics: Theory of sets, Hermann (original), Addison-Wesley (translation).