OPEN MATHEMATICS, IN PRACTICETRURETURING / THE OMEGA INSTITUTE

AN OPEN MATH COLLABORATION

Human intelligence.
Machine rigor.
An endless loop.

Start with human intuition. Explore with AI. Ground it in Lean. Let every checked result inspire the next question.

See how the loop works

THE RESEARCH CONTINUES

HUMAN DIRECTIONAn intuition worth exploringIntuition · questions · context

MACHINE DISCIPLINEA checkable contributionRead sources · construct arguments · check proofs

SHARED KNOWLEDGEA result to build onReview · reuse · the next question

01 → 02 → 03 →Every result feeds the next question.

01 / WHY WE BUILT THISTRURETURING / THE OMEGA INSTITUTE

Ideas begin as intuition.
We give them a precise place to stand.

We have more ideas about the world than we can make precise on our own.

AI helps us explore, find connections and read the relevant work. A convincing chain of thought still needs a proof.

LEAN FORMALIZATION

Explicit definitions.
Checked logic.
Reusable results.

Make one relation precise, then build on it.

01
Bring an intuition
A question, a pattern, a possible connection.
02
Explore and read
Agents find sources. We study the definitions and sharpen the question.
03
Formalize and reuse
State the assumptions. Check the proof. Preserve its dependencies.
04
Help solve a real problem
Work on someone else’s conjecture. Their feedback opens the next question.

A result becomes the next starting point.

A SHARED STARTING POINT

We connect knowledge through logical relationships, without partitioning it by discipline.

02 / CORRECTNESS AND CONTRIBUTIONTRURETURING / THE OMEGA INSTITUTE

The proof checks out.
What have we learned?

01 / CHECK THE REASONING

Is the reasoning correct?

Lean checks the proof under explicit definitions and assumptions.

02 / CHECK THE CONTRIBUTION

What does this add?

Renaming an existing theorem gives us a valid proof, but no added understanding.

INFORMATION ESCAPE

What differences do our current concepts fail to capture?

Lean checks whether the reasoning is correct. Correctness alone does not tell us what a contribution adds: renaming an existing theorem can pass the proof checker without adding understanding. We therefore ask what the contribution adds to existing knowledge. Information escape studies which differences the current concepts fail to capture. The next slide makes this concrete with two graphs. Formal verification checks the encoded proposition under its stated assumptions. Evaluating additional understanding also requires checking the source problem, prior work and substantive proof content. Information escape studies one precise part of that question: the distinctions a concept catalog captures on a fixed state space. It is not a universal score for theorem novelty. Bind-only review separately checks that substantive work occurs on the live proof path. The next two slides show the concept-catalog metric with a concrete example.

03 / THE CORE: DISTINCTIONTRURETURING / THE OMEGA INSTITUTE

Information escape:
differences our knowledge cannot see.

Different states give identical readings under every selected concept. Here, the catalog records degree sequence alone; it misses the difference between these graphs.

G₁

One six-cycle

Degree at every vertex2

Is it connected?Yes

G₂

Two triangles

Degree at every vertex2

Is it connected?No

INFORMATION ESCAPE

A real difference left uncaptured by our concepts.

x ≠ y, ∀ i ∈ S, cᵢ(x) = cᵢ(y)

Formal escape definition ↗

Information escape is intrinsic to a fixed state space X and selected catalog S: E_S = {(x,y): x ≠ y and every c_i in S gives equal readings on x and y}. The catalog concepts are derived from registered mathematical primitive bundles, not arbitrary labels attached to proofs. No external question is needed: the reference is state identity. The example fixes X to exactly two graphs and S to their sorted degree sequence. The graphs differ but both readings are (2,2,2,2,2,2), so both ordered distinct pairs escape. Connectedness makes their difference visible to the viewer; it is not an additional selected readout. Escape means the difference remains unrepresented by this catalog. If every available definition merges a pair, combinations of those definitions cannot separate it: extend the representation. The graph example illustrates the definition; it is not a new research claim.

04 / FROM DISTINCTION TO INFORMATION GAINTRURETURING / THE OMEGA INSTITUTE

A concept’s contribution:
the difference we lose without it.

THE SAME TWO GRAPHSTwo-state illustration

G₁

G₂

Degree sequence(2,2,2,2,2,2)(2,2,2,2,2,2)

2 / 2

escape rate in this two-state arena

Two different graphs; identical concept readings. Both ordered pairs escape.

Still-indistinguishable different pairs / all different pairs (ordered).

01 / A NEW NAME PRESERVES THE SAME BLIND SPOT

Any function of the same degree sequence still gives the same answer on both graphs.

02 / CAPTURE A PREVIOUSLY INVISIBLE DIFFERENCE

Triangle count separates these two graphs: 0 versus 2. It reads a relation the degree sequence lost.

03 / REMOVE IT: DOES THE DIFFERENCE ESCAPE AGAIN?

Remove triangle count: the two graphs become indistinguishable again. This isolates what that concept contributes beyond the rest.

δᵢ = ε(S ∖ {i}) − ε(S)

Contribution gain = escape without it − escape with it. Here: 1 − 0 = 1.

FORMAL FOUNDATIONSEscape rate & contribution gain ↗Distinction & escape gain ↗Blind-language obstruction ↗

For a fixed finite arena X with at least two states, ε(S) = |E_S| / (|X|(|X|−1)): the fraction of ordered different pairs still indistinguishable under all selected concepts. This two-graph example gives 2/2 with degree sequence alone, still 2/2 after relabeling, and 0/2 after adding triangle count. The full illustrated catalog contains degree sequence and triangle count. Removing triangle count raises escape from 0 to 1, giving its leave-one-out gain of 1. Removing degree sequence while retaining triangle count gives gain 0. Gain is relative to the same current catalog, not a comparison between historical submissions. The formal finite-catalog criterion equates positive gain with unique capture, strict kernel refinement and nonrecoverability from the remaining catalog. The example does not itself certify a novel theorem. Bind-only separately checks proof shape and substantive content on the live proof path. State space and denominator stay fixed; deleting difficult states would change the evaluation rather than demonstrate capture.

05 / HOW THE HARNESS ENFORCES THE METHODTRURETURING / THE OMEGA INSTITUTE

A harness for
correctness and contribution.

THE MECHANISMWHAT IT REQUIRESWHY IT MATTERS

01

References before proofs

Search literature, our library, pinned mathlib and third-party Lean libraries. Check assumptions; directly cite and apply exact matches.

Build on what is known.

02

Formal verification

State the claim and assumptions in Lean. Check the proof term and its axiom dependencies in the kernel.

Establish that it follows.

03

Reject bind-only

Expand aliases and local helpers. Reject mere instantiation, projection or repackaging as new mathematical content.

Require a substantive step.

04

Information escape

Count different states the catalog still cannot distinguish. Remove a contribution to test whether its distinction is supplied by the rest.

Identify its unique contribution.

Checked contributions return to the library with their sources and dependencies, ready for the next researcher or model.

Read the harness rules ↗

06 / IDEAS ARE BECOMING SHARED MATHEMATICSAS OF 01 OCT 2026

Real problems. Real papers.
A growing research conversation.

439Open-problem resolutions recorded

30+Researchers in dialogue and feedback

4Joint papers on arXiv

$First page of the joint Padovan recurrence manuscript.$

WITH BENOIT CLOITRE

A Padovan-automatic description of a nested recurrence

A counterexample grew into a joint theorem, independent verification and a reusable Lean archive.

arXiv:2609.33421 ↗

$First page of Sub-quorum colorings of graphs, arXiv version 3.$

WITH RAFIK SAHBI

Sub-quorum colorings of graphs

From a formal hypercube proof to grid certificates, structural bounds and a shared paper.

arXiv:2609.25128v3 ↗

SAIR EQT2Official #1 · 200/200 in all four participations

Solver & run records ↗Results and sources ↗

NeurIPS 2026 Math-AI WorkshopAccepted for poster presentation

Cross-Engine Admission Contracts for Autonomous Formalization

Early work on our harness engineering.

As of October 1, the recorded problem registry contains 439 unique problem IDs: 336 proved and 103 refuted. This is a record of problem resolutions, including counterexamples, not 439 positive proofs or necessarily 439 previously unknown results. The currently deployed research catalog contains 427 released resolutions; publication lags the registry. The public count manifest lists the 439 IDs and original question sources without correspondence. Four joint arXiv preprints are publicly verified: the Padovan recurrence paper with Benoit Cloitre, the sub-quorum coloring paper with Rafik Sahbi, and two earlier community collaborations with Manuel Israel Cázares on mechanism-level routing and the EQT2 solver. The two manuscript previews show selected recent papers. The Math-AI workshop poster is listed separately and is not included in this arXiv count. Thirty-plus reflects 38 named researchers in research exchanges, proof review, specific verification requests, positive acknowledgement or expressed interest in reviewing the work. It includes copied coauthors already recorded in substantive two-way threads; names are deduplicated. This does not imply 38 agreed collaborations or independent replies from every participant. Institutional labels identify individual researchers, not institutional partnerships or endorsements. Campbell’s current OpenAI affiliation was directly confirmed in correspondence. Rust and Ramgoolam’s UK affiliations are stated in their source papers; Zhang’s NUS affiliation is stated in his source paper. The images are real first-page crops: the archived Cloitre manuscript and Sahbi arXiv v3. The next slide shows the reciprocal research behind these results. The official EQT2 submission page supplied by the team owner lists four participations, each with official rank #1 and score 200/200: Solo and Marathon, each with Google: Gemma 4 31B and OpenAI: gpt-oss-120b. The separate 1889/1889 figure belongs to internal testing and is not the official competition score. The solver used zero LLM calls. Model names identify participation settings. The source manifest records this distinction and the user-provided provenance without account details. Cross-Engine Admission Contracts for Autonomous Formalization, by Haobo Ma and Wenlin Zhang, was accepted for poster presentation at the NeurIPS 2026 Math-AI Workshop, as confirmed by the author on October 1. The supplied manuscript was checked for title, authors and scope. It presents earlier harness engineering: kernel validity, allowed dependencies and statement faithfulness require distinct checks. It is not a complete account of the current Trureturing methodology.

07 / RESEARCH DIALOGUE AND RECOGNITIONAS OF 01 OCT 2026

Research, review and recognition

John M. CampbellOpenAIExplicit formulas and recursive information

Rafik SahbiUniversity of CarthageHypercube proof and uniform grid bounds

Benoit CloitreOEIS contributorPadovan recurrences and Conway-type dynamics

Louxin ZhangNational University of SingaporeMinimal word neighborhoods and classification

Reza NikandishJundi-Shapur University of TechnologyDimension six: 12 line colors, 15 subspace colors

Max A. AlekseyevGeorge Washington University · OEISTranslation-action proof and formalization feedback

Sanjaye RamgoolamQueen Mary, LondonGraph determinants and geometric multiplicities

Peter CameronUniversity of St AndrewsReviewed our semigroup counterexample

Robert IsraelUniversity of British Columbia · OEISProof feedback and OEIS update support

Wieb BosmaRadboud UniversitySumfree periodic families and finite certificates

R. VenkateshIndian Institute of ScienceHypergraph positivity and sunflower conditions

Václav KotěšovecOEIS · AsymptoticsHankel constants, precision checks and OEIS links

Joint research, proof review and feedback from researchers.Results and sources ↗

This selection includes joint research, proof review and recognition of contributions. Max A. Alekseyev found the translation-action argument an interesting alternative viewpoint and suggested more challenging examples; the existing OEIS formula already implies the divisibility result. Peter Cameron reviewed the five-element semigroup counterexample note and found the argument sound. Robert Israel offered OEIS updates and attribution. Václav Kotěšovec welcomed the analytic Hankel-constant results, supplied a high-precision numerical calculation and asked to link the note in OEIS. His next-order question led to further written results on fixed and growing shifts; no joint authorship has yet been agreed. These are individual exchanges, not institutional endorsements or agreed joint papers. The source manifest records 38 named contacts, including existing copied coauthors and newly verified feedback. Complete correspondence remains private.

08 / GROWTH & FOUNDATIONSTRURETURING / THE OMEGA INSTITUTE

Connected knowledge.
A growing white-box model.

CUMULATIVE FROZEN THEOREM STATEMENTS

35,010

27 days · 2.32×+19,897 theorem statements

OUR RESEARCH THESIS

Mathematics is logical structure.

Shared logic · information escape

Relations of relations · recursion

Spacetime · holographic geometry

A shared library of nontrivial reasoning. Definitions, assumptions and proofs stay explicit.

$A real dependency network of reusable formal modules.$

Relations compose across disciplines. The dependency graph records how each checked result builds on others.

Explore the shared knowledge ↗

The chart counts unique theorem statement_id values in schema-v5 Freeze records under Golden/Frozen/accepted, using published source commits from the Library history. It counts archived frozen statements, including retained historical versions, not modules, solved problems or distinct mathematical ideas. The source period is September 2–29, 2026: 15,113 to 35,010, a 2.32-fold increase. The chart uses real source timestamps, a linear y-axis and a zero baseline; no extrapolation. The research thesis is an orientation: finite descriptions and fixed observation scales motivate studying their residuals and extending representations. A single injective readout can distinguish a specified state space; inevitability of escape needs the relevant capacity, language or diagonalization assumptions. Recursive relations, contextual spacetime and holographic geometry name research programs documented in the linked source manifest, not a claim that all those manuscripts are fully formalized. The method repeatedly turns uncaptured relations into definitions and checked contributions. The proposed collaboration combines mathematician-led direction, OMM and open participation. Our research premise is that knowledge connects through shared logical structures. We organize the library through explicit relationships rather than disciplinary partitions. In this sense the library is a growing white-box model: its definitions, premises, proofs and dependencies can be inspected and composed. Gathering all nontrivial logical relationships is the guiding ambition. The working method keeps finding missing distinctions and extending the library. Model here names this explicit body of reasoning, rather than a claim of complete coverage or an autonomous inference engine.

09 / OPEN SOURCE. OPEN CONTRIBUTION.TRURETURING / THE OMEGA INSTITUTE

You can start before you are an expert.
Learn by making one step precise.

01

A question

Give the research a direction.

02

An example

Expose a missing distinction.

03

An argument

Develop the next proof step.

04

A formalization

Make the reasoning checkable.

05

An independent check

Reproduce and strengthen the result.

10 / THE PEOPLE BEHIND THE WORKTRURETURING / THE OMEGA INSTITUTE

Building Trureturing.
Together.

AGENT INFRASTRUCTURE

Haobo Ma

CEO · Chrono AI

Builds infrastructure for agents to access tools, reuse skills and work together, with explicit checks on their progress.

OPEN SOURCE PRODUCTS

NyxID ↗Ornn ↗chrono-harness ↗

PHYSICS + AI RESEARCH

Wenlin Zhang / Lexa

PhD student · National University of Singapore

Pursues de novo protein design through physics and AI, studying how structure, dynamics and energetics connect to biological function.

RESEARCH FOCUS

Protein design · Dynamics · Thermodynamics

We build the tools and pursue the research, learning how human–AI collaboration can produce knowledge that others can check and build on.

11 / THE SAIR COLLABORATION PROPOSALTRURETURING / THE OMEGA INSTITUTE

Connect OMM to this research loop.
More questions. More people building on the results.

MATHEMATICIANS + SAIR

Questions, expertise and open models

Researchers choose meaningful directions and review the mathematics. SAIR brings its open-model effort and research community.

TRURETURING

A white-box library and research harness

A connected library of explicit reasoning, with a harness to check, extend and reuse it through open contribution.

WHAT WE BUILD TOGETHER

An open contribution loop

Real questions guide model reasoning.
The harness requires correctness and substantive contributions.
Researchers review the results and set the next direction.
Each checked contribution extends the shared white-box model.

THE ASK

Connect OMM to our harness and develop a shared research track with mathematicians and open contributors.

12 / CHOOSE THE NEXT QUESTION TOGETHERTRURETURING / THE OMEGA INSTITUTE

LET’S BUILD THE NEXT COLLABORATION

Start with one idea.
Make one step precise.

Let OMM help more people turn intuition into checked, reusable knowledge. Every contribution gives the next person a place to begin.

Start a research contribution ↗Explore the open repository ↗

THE FIRST WORKING SESSION

01Choose a question together
02Connect the model to the harness
03Open the work to contributors

Human intelligence.Machine rigor.An endless loop.

Ideas begin as intuition.We give them a precise place to stand.

Explicit definitions.Checked logic.Reusable results.

Bring an intuition

Explore and read

Formalize and reuse

Help solve a real problem

The proof checks out.What have we learned?