User:Boris Tsirelson/Sandbox1: Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Boris Tsirelson
No edit summary
No edit summary
 
(411 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>
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.


 
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).
[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]
 
{{Image|Isabelle1.png|right|350px|The graphical user interface started.}}
 
 
 
 
 
 
The graphical user interface started.
 
 
 
 
{{Image|Isabelle2.png|left|350px|The source file is read.}}
 
 
 
 
&nbsp;&nbsp;The source file is read.
 
{{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"