User:Boris Tsirelson/Sandbox1: Difference between revisions
imported>Boris Tsirelson No edit summary |
imported>Boris Tsirelson No edit summary |
||
Line 2: | Line 2: | ||
''"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> 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 computers a programmer is able to debug only very simple programs. | ''"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> 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 computers a programmer is able to debug only very simple programs. | ||
A '''proof assistant''' is a computer program used interactively for developing human-readable reliable mathematical documents in a formal language. | |||
Nowadays (about 2010) the most successful project of this class combines | |||
* ''Isabelle,'' a generic system for implementing logical formalisms; | |||
* ''Isar'' (Intelligible SemiAutomated Reasoning), a versatile language environment for structured formal proofs; | |||
* ''Proof General,'' a configurable user interface (front-end) for proof assistants; | |||
* HOL (Higher-Order Logic). | |||
[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] + |
Revision as of 14:56, 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] 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 computers a programmer is able to debug only very simple programs.
A proof assistant is a computer program used interactively for developing human-readable reliable mathematical documents in a formal language.
Nowadays (about 2010) the most successful project of this class combines
- Isabelle, a generic system for implementing logical formalisms;
- Isar (Intelligible SemiAutomated Reasoning), a versatile language environment for structured formal proofs;
- Proof General, a configurable user interface (front-end) for proof assistants;
- HOL (Higher-Order Logic).
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).