Formal Proof Data
On this page
- Publish the Lean sources OCME actually uses.
- Formal evidence catalogue
- mko-tends-to-relation
- Limitations and excluded scope
- mko-euclid-pythagorean-theorem
- Limitations and excluded scope
- mko-euclid-pythagorean-theorem
- Limitations and excluded scope
- mko-set-membership
- Limitations and excluded scope
- mko-function-mapping
- Limitations and excluded scope
Acceptance of a proof term by the Lean kernel does not automatically prove the full encyclopedia prose, the natural-language semantic bridge, or every equivalent geometric representation. This catalogue publishes both passed checks and open boundaries.
Publish the Lean sources OCME actually uses.
The public set contains OCME-owned Lean sources, the pinned toolchain, Lake project configuration, and the dependency lock. It excludes .lake, downloaded Mathlib source, packages, and build caches. Lake retrieves the pinned dependencies during replay.
View SHA-256 manifest
Formal evidence catalogue
mko-tends-to-relation
For every function f : α → β and filters l₁ and l₂, Filter.Tendsto f l₁ l₂ is equivalent to Filter.map f l₁ ≤ l₂.
evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d · passed
Limitations and excluded scope
- This evidence formalizes Mathlib's filter semantics for convergence. The bare notation x → a must first specify source and target filters before it can be connected to this statement.
- It is not by itself an epsilon-delta definition, and it does not prove the limit of any particular function.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.
View raw Evidence JSONmko-euclid-pythagorean-theorem
In every real inner product space, if the angle between vectors x and y is π/2, then the squared norm of their sum equals the sum of their squared norms.
evidence-sha256-4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752 · passed
Limitations and excluded scope
- This evidence proves the vector core theorem. A separate side-length theorem supplies the explicit bindings for a, b, and c.
- The evidence depends on Lean 4.30.0, Mathlib v4.30.0, and the declared imported module.
- A formal proof does not replace review of the encyclopedia wording, symbol roles, or geometric model.
View raw Evidence JSONmko-euclid-pythagorean-theorem
For every real inner product space, vectors x and y, and real numbers a, b, and c, if x and y meet at angle π/2 and a = ‖x‖, b = ‖y‖, c = ‖x + y‖, then a·a + b·b = c·c.
evidence-sha256-701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e · passed
Limitations and excluded scope
- This evidence closes the side-length model declared by OCME; it is not automatically identical to every affine-plane, coordinate, or triangle construction.
- The hypotenuse length is defined as the norm of the vector sum. Other vertex orderings require a separate equivalence proof.
- The evidence depends on Lean 4.30.0, Mathlib v4.30.0, and the pythagorean_vector theorem.
View raw Evidence JSONmko-set-membership
For every type α, element x : α, and set A : Set α, the proposition x ∈ A is equivalent to evaluating the predicate A x.
evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d · passed
Limitations and excluded scope
- This evidence formalizes Lean's representation of Set as α → Prop; it does not claim to cover every foundation of set theory.
- A membership test in a programming container does not therefore become general mathematical set membership.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.
View raw Evidence JSONmko-function-mapping
For every pair of types X and Y, function f : X → Y, and input x : X, there exists a unique y : Y such that f x = y.
evidence-sha256-d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b · passed
Limitations and excluded scope
- This evidence formalizes the existence and uniqueness of output for Lean total functions; it does not cover partial functions, random procedures, or effectful programs.
- The codomain Y and the actual range of f remain different concepts; the theorem does not claim that f is surjective.
- The evidence depends on Lean 4.30.0 and Mathlib v4.30.0.
View raw Evidence JSON