User:Boris Tsirelson/Sandbox1

From Citizendium
< User:Boris Tsirelson
Revision as of 06:27, 9 August 2010 by imported>Boris Tsirelson
Jump to navigation Jump to search

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)."[1] Reliability of these experience and flair appear to be high but not perfect. Formalization is especially desirable in complicated cases, but feasible only in very simple cases, unless computers help. Similarly, without a computer a programmer is able to debug only very simple programs.


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.

Notes

  1. ↑ Bourbaki 1968, page 8.

References

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

Retrieved from "https://citizendium.org/wiki/index.php?title=User:Boris_Tsirelson/Sandbox1&oldid=628602"