Results and Exemplars
Public records for results, verification surfaces, bounded certificates, reconstruction archives, and end-to-end exemplars. This page is an index; authority remains in the linked records.
How to read this page
The entries below are grouped by support type. They are not ranked by importance.
A result belongs here only when the public record states what crossed the boundary and what did not. Publication, merge, or visual prominence does not strengthen the mathematical claim.
VGSE-001 · restricted four-claim publication
Support class: qualified restricted successor route
Protected scope: VGSE-C00, VGSE-C01, VGSE-C04, VGSE-C05
Excluded claim: VGSE-C06
The successor route MC-ROUTE-VGSE-001-R4 qualified exactly four claims. The original five-claim route remains unchanged and fail-closed on VGSE-C06.
The retained C06 boundary matters. The published source package does not establish the Figure-16-to-pinned-C correspondence required to reopen that claim. The restricted result therefore does not qualify the original five-claim route by implication.
The publication creates no authority for rigid foldability, collision freedom, finite thickness, manufacturing, novelty, patentability, product performance, or commercial value.
The programme has since opened a separate engineering-discovery lane. That lane starts from the bounded protected result and does not broaden it.
Inspect the current engineering handoff
Verified corpus · OpenAI Ten Proofs
Support class: protected formal verification record
Verified subject: exact supplied Lean corpus at the pinned upstream revision
MATHCERT rebuilt all ten supplied Lean modules and checked the twelve advertised headline declarations through the Lean kernel. The public record pins the source tree, toolchain, module identities, permitted axioms, independent review, protected merge, and post-merge replay.
The verification does not claim line-by-line semantic equivalence with every prose statement in the source exposition. It does not create novelty or priority claims for the underlying mathematics.
Fixture 003: The logarithmic GCD kernel
Publication ID: PUB-LOG-GCD-001
Support class: Classical mathematics · certified formal artifact
Publication status: published
Claim boundary: No novelty or priority claim
The published identity is
K(m,n) = log(gcd(m,n)) = <phi(m), phi(n)>
for the declared positive-input domain and finitely supported divisor feature vector.
The public record separates the certified formal artifact from mathematical history. It makes no claim that the theorem, kernel, feature representation, or proof idea is new.
Read the publication record · Read the prior-art audit
Solved-problem archive · Poincaré reconstruction
Support class: qualified reconstruction archive for a solved classical theorem
This archive records a bounded reconstruction route and its supporting documentary material. It is not presented as a new proof of the Poincaré conjecture and does not assign novelty to the reconstructed mathematics.
Read the reconstruction archive · Read the documentary edition
End-to-end proof traces
These traces test whether the programme can preserve source identity, proof structure, executable checking, and reader-facing explanation through a complete bounded route.
Euclidean GCD
The Euclidean GCD trace is a compact end-to-end proof artifact. Its value is institutional: the mathematics is elementary enough that the programme machinery can be inspected without confusing governance complexity with theorem difficulty.
Read the Euclidean GCD proof trace
Linear Diophantine solvability
The linear Diophantine trace extends the same method to a second classical statement with an explicit proof and checking route.
Read the linear Diophantine proof trace
Executable fixtures
Fixtures test local programme claims about translation, checking, model classes, and certificate handling. They are not substitutes for the larger theorem programmes.
UF-INV-001 · exact algebraic identity
The fixture checks an exact polynomial identity over the declared field setting. It keeps the semantic translation and the exact arithmetic witness as separate support boundaries.
RAD-NIL-002 · radical membership and model-class boundary
The fixture distinguishes a valid field-level implication from its false generalization to all commutative Q-algebras. The countermodel is part of the retained result.
What does not belong on this page
The following states belong elsewhere until their support changes:
- an active work package with an unresolved theorem dependency;
- a promising computation without the required bridge;
- a source reconstruction that has not crossed a certification boundary;
- a visual explanation without independently governed evidence;
- a merged document whose mathematical claim remains open;
- an engineering hypothesis without a validated experiment or derivation.
Use Current Work for live obligations and Mathematical Estate for standing programmes, domains, and archives.