User:Boris Tsirelson/Sandbox1: Difference between revisions
imported>Boris Tsirelson No edit summary |
imported>Boris Tsirelson No edit summary |
||
| Line 1: | Line 1: | ||
For a [[theory (mathematics)|mathematical theory]], correctness means formalizability. | For a [[theory (mathematics)|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)."<ref>{{harvnb|Bourbaki|1968|loc=page 8}}.</ref> | |||
[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle] + | [http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle] + | ||
| Line 59: | Line 61: | ||
{{Image|Isabelle15.png|right|350px|...and the theorems.}} | {{Image|Isabelle15.png|right|350px|...and the theorems.}} | ||
==Notes== | |||
{{reflist|2}} | |||
==References== | |||
{{Citation | |||
| last = Bourbaki | |||
| first = Nicolas | |||
| title = Elements of mathematics: Theory of sets | |||
| year = 1968 | |||
| publisher = Hermann (original), Addison-Wesley (translation) | |||
}}. | |||
Revision as of 06:21, 9 August 2010
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]
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
The graphical user interface started.
The source file is read.
Definitions are processed; the formulation of the first lemma is being processed.
The formulation of the first lemma is processed; the goal is pending.
Notes
- ↑ Bourbaki 1968, page 8.
References
Bourbaki, Nicolas (1968), Elements of mathematics: Theory of sets, Hermann (original), Addison-Wesley (translation).