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 recordDiscover
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.