User:Boris Tsirelson/Sandbox1: Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Boris Tsirelson
No edit summary
 
(367 intermediate revisions by one other user not shown)
Line 1: Line 1:
For a [[theory (mathematics)|mathematical theory]], correctness means formalizability.
{{AccountNotLive}}
''"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 appears 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.)
The [[Heisenberg Uncertainty Principle|Heisenberg uncertainty principle]] for a particle does not allow a state in which the particle is simultaneously at a definite location and has also a definite momentum. Instead the particle has a range of momentum and spread in location attributable to quantum fluctuations.


A '''proof assistant''' is a computer program used interactively for developing human-readable reliable mathematical documents in a formal language. (It is not the same as a non-interactive, fully automated theorem prover.)
An uncertainty principle applies to most of quantum mechanical operators that do not commute (specifically, to every pair of operators whose commutator is a non-zero scalar operator).
 
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).
 
This combination is meant below (unless otherwise stated explicitly), and called just ''Isabelle'' (rather than ''Isabelle/Isar/HOL/Proof General'').
 
[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle] +
[http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems] +
[http://isabelle.in.tum.de/ Isabelle] +
[http://isabelle.in.tum.de/download.html Download and installation] +
[http://isabelle.in.tum.de/projects.html Projects] +
[http://isabelle.in.tum.de/library/ The Isabelle2009-2 Library] +
[http://isarmathlib.org/ IsarMathLib: A library of formalized mathematics for Isabelle/ZF]
 
==Example session==
 
===First impressions===
 
An existing file, verified before, is used as the source text in this example. Thus, the session is not really interactive. However, this fact is not known to ''Isabelle.'' The proof assistant treats the session as interactive, and the text as new.
 
We start ''Proof General'' (Fig. 1) and enter the source text (Fig. 2).
 
{| align=center
|-
|
{{Image|Isabelle1.png|left|350px|Fig. 1: ''Proof General'' welcome}}
{{Image|Isabelle2.png|right|350px|Fig. 2: Source text entered}}
|}
 
On this stage ''Proof General'' does not send the text to ''Isabelle''; we still can edit the text. ''Proof General'' helps us by automatic colorization according to the syntax of the ''Isar'' language.
 
We start a new theory "CauchysMeanTheorem". (The well-know [[Algebraic-geometric mean inequality|Cauchy's Mean Theorem]] says that the geometric mean is less than, or equal to, the arithmetic mean, for every finite collection of positive numbers. However, this theorem will appear much later, near the end of the source text.) The existing theory "Complex_Main" is a prerequisite. (It contains main facts about real and complex numbers; only real numbers are relevant, but some useful formulas about <math>(a+b)^2</math> appear in "Complex_Main".)
 
Clicking the red button "<math>\triangleright</math>" we send the first portion of the text to ''Isabelle.'' After two more such clicks ''Isabelle'' reads the line "imports Complex_Main" and finds in the library the "Complex_Main" theory (since it is a prerequisite to the new "CauchysMeanTheorem"), but also "Real", since it appears to be a prerequisite to "Complex_Main", and so on, recursively, until all prerequisites are found and processed (in a logical order). After 9 more clicks we come to the screen shown on Fig. 3. The definitions (and everything before them) are already processed by ''Isabelle''; accordingly, they turn into blue, and become read-only. The formulation of the first lemma is being processed by ''Isabelle''; accordingly, it turns into orange. A fraction of a second later we get Fig. 4. The formulation of the lemma is read by ''Isabelle''; a dialog about its proof starts on the bottom window.
 
{| align=center
|-
|
{{Image|Isabelle3.png|left|350px|Fig. 3: Definitions are done; now reading the lemma.}}
{{Image|Isabelle4.png|right|350px|Fig. 4: The proof mode started.}}
|}
 
===A robot as a student===
 
The first lemma "listsum_empty" (of the new "CauchysMeanTheorem" theory) is ridiculously trivial; it claims that the sum of the empty collection of numbers is equal to zero!
 
A human student starting to learn Cauchy's mean theorem
:<math> \sqrt[n]{a_1\dots a_n} \le \frac{a_1+\dots+a_n}n </math>
is supposed
 
===More===
 
 
--------------------------------------------------
 
{{Image|Isabelle3.png|right|350px|Definitions are processed; the formulation of the first lemma is being processed.}}
 
 
 
Definitions are processed; the formulation of the first lemma is being processed.
 
{{Image|Isabelle4.png|left|350px|The formulation of the first lemma is processed; the goal is pending.}}
 
The formulation of the first lemma is processed; the goal is pending.
 
{{Image|Isabelle5.png|right|350px|At last, a really serious lemma.}}
 
{{Image|Isabelle6.png|left|350px|The goal.}}
 
{{Image|Isabelle7.png|right|350px|"We have", why?}}
 
{{Image|Isabelle8.png|left|350px|Here is why!}}
 
{{Image|Isabelle9.png|right|350px|Really complicated arguments...}}
 
{{Image|Isabelle10.png|left|350px|Happy end is coming.}}
 
{{Image|Isabelle11.png|right|350px|The theorem is proved.}}
 
{{Image|Isabelle12.png|left|350px|Some options of the Proof General.}}
 
{{Image|Isabelle13.png|right|350px|Isabelle, show us your methods...}}
 
{{Image|Isabelle14.png|left|350px|...and your term bindings...}}
 
{{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)
}}.

Latest revision as of 03:25, 22 November 2023


The account of this former contributor was not re-activated after the server upgrade of March 2022.


The Heisenberg uncertainty principle for a particle does not allow a state in which the particle is simultaneously at a definite location and has also a definite momentum. Instead the particle has a range of momentum and spread in location attributable to quantum fluctuations.

An uncertainty principle applies to most of quantum mechanical operators that do not commute (specifically, to every pair of operators whose commutator is a non-zero scalar operator).

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