Language:PortuguêsEnglish

Verified science

Quantum facts, with the proof attached.

Known quantum-mechanics results, checked step by step by a proof assistant. Click any fact to see the Lean theorem.

What this is — and what it is not

These tools show machine-checked formal verifications (Lean 4 + mathlib, zero `sorry`) of known quantum-mechanics results. This is not new physics: it is auditable proof of established theorems. Each fact carries its source and an honesty note.

Verified facts

Each card is a known result with a machine-checked proof. The proof is the exact Lean theorem — no hand-waving.

Corpus audited at export: 82 Lean files · 313 theorems/lemmas · 0 with `sorry`.

  • GHZ paradox: with 3 particles, the quantum prediction contradicts any local hidden-variable model with certainty (deterministic, not statistical).

    nonlocalityall-vs-nothingdeterministic

  • Tsirelson bound: quantum correlations violate the CHSH inequality, but never above the exact ceiling 2√2 ≈ 2.828.

    nonlocalitychshbound

  • Contextuality (Kochen–Specker via the Mermin square): it is impossible to consistently assign definite values to all measurements at once.

    contextuality

  • No-cloning theorem: there is no operation that copies an arbitrary unknown quantum state.

    no-go

  • For a single system, real numbers suffice: complex QM is simulated by dimension doubling (i ↦ J, with J² = −1), and ℂ embeds faithfully into real 2×2 matrices.

    real-vs-complexsingle-system

  • Local tomography selects complex: counting state parameters (real d(d+1)/2, complex d², quaternionic 2d²−d), only complex QM is locally tomographic.

    real-vs-complextomography

  • How many ±1 observables pairwise anticommute: complex admits three (σx, σy, σz), real at most two. The 'imaginary dimension' (σy) is what real lacks — the algebraic root of the network separation.

    real-vs-complexanticommutation

Causal-order certifier

Describe who signals to whom between the parties. The certifier decides whether the causal order is definite (acyclic, with a time function) or indefinite (a causal loop), and emits a Lean certificate you can verify with `lake`.

Examples:

One per line or comma-separated, as i->j (e.g. 0->1, 1->2).

sumno is an academic research assistant.

Search millions of papers, summarize abstracts, and export references.

Create account