Operator algebras
Naimark's problem
A proposed ZFC construction of a single C*-algebra with one irreducible equivalence class and a faithful separable tracial representation.
Read the project recordAN INDEPENDENT RESEARCH INITIATIVE
Exact Mathematics
with AI
Mathematical discovery, formal verification, and human understanding.
An independent research initiative exploring mathematics with AI. We share preliminary results, develop reusable formal mathematics, and build explanations that help readers understand proofs. Each project records its verification status and how that status changes over time.
Research in progress
Follow a result from its first precise statement to a proof that can be checked, understood, and reused.
Geometry of normed spaces
Sphere Rigidity
A study of how the metric structure of a unit sphere determines its ambient real normed space, with a separate route toward reusable proof tools.
Read the project recordTOPICS
Read a proof, step by step.
Expository notes that make the ideas and dependencies of an argument easier to follow.
GEOMETRY OF NORMED SPACES
Tingley’s problem: the chord argument
A reader’s reconstruction of the argument in OpenAI’s preprint, from the radial distance defect to a direct comparison of aligned chords.
Read the introduction and noteFIXED POINTS IN BANACH SPACES
Reading OpenAI’s fixed-point argument
A detailed reconstruction through ordered trees, root responses and finite switching, with an RNP extension and no priority claim.
Introduction, reading route and PDFBROUWER–SCHAUDER FIXED POINTS
Brouwer's Fixed-Point Theorem from Commuting Operators
An operator-and-polynomial proof of Brouwer's fixed-point theorem, followed by a direct passage from the cube theorem to Schauder's compact-image theorem.
Introduction, reading route and PDFLIPSCHITZ-FREE SPACES
Lipschitz-Free Spaces over Hilbert Spaces
A detailed introduction to Lipschitz-free spaces, from linearization and compact reduction to the absence of c0 in the free space over a real Hilbert space.
Introduction, reading route and PDFLIPSCHITZ HOMEOMORPHISMS
Reading OpenAI's Construction of Lipschitz Homeomorphic but Linearly Nonisomorphic Separable Banach Spaces
A Lipschitz homeomorphism preserves distances up to multiplicative constants, but it need not preserve the linear structure of a Banach space. This Expository Note reconstructs OpenAI's counterexample for separable real Banach spaces and explains how the construction fits together, from Lipschitz-free-space inputs to weighted graph spaces and an explicit nonlinear change of variables.
Introduction, reading route and PDFDiscover
Share mathematical claims and proofs without waiting for the final form of a journal article. State what is known, and what still needs checking.
Verify
Keep formal checking and statement alignment visible as separate records. A new version should say exactly what changed.
Understand
Make the necessary definitions and intermediate results reachable from the proof itself. The aim is mathematics that readers can learn and reuse.
MATHLIBANNEX
Let one proof help the next.
MathlibAnnex connects reusable Lean declarations with Declaration Cards, exact source views, and four guided Project overviews.
MathlibAnnex hubPrecision without a black box.
A reader should be free to skip familiar details—and able to open the details that are not yet familiar.