Connect and verify
Living mathematical knowledge and reusable formal libraries.
Samplinglib · Math 2.0
Proofs that grow human understanding.
A living network and a reusable Lean library for sampling, optimisation, and geometry. Read the mathematics, explore its mechanisms, and check its assumptions.
Our original goals of connected knowledge, reusable Lean proofs and clearer teaching predate and resonate with Terence Tao's October 2026 lecture. His examples on slides 22 and 25–26 provide a shared reference for our work and next questions.
We welcome collaborators in probability, geometry, education and mathematical AI to improve the explanations and test what proof maps can reveal.
Explain and teach
Motivated exposition and interactive learning built on proof structure.
Explore and test
Cross-pollination, proof ablation, theorem neighborhoods and model boundaries.
Concrete contributions
Nine directions, one connected foundation
Current foundations are linked below. Next contributions are research work to undertake; their own evidence is required before claiming completion.
01Open exposition problemsUnderstanding
Explain the mechanism behind sampling proofs, not just their endpoints.
Current foundation. Source-aligned readers and the Functor Hypergraph expose assumptions and recurring mechanisms.
Next contribution. Choose an opaque argument; publish a motivated explanation with a checked path to its full proof.
Read semigroups and functional inequalities →02A living knowledge networkFoundation
Connect scattered books and frontier papers through reusable mathematical structure.
Current foundation. Library shelves, SampleWiki cases, source anchors and the shared graph organize ongoing work.
Next contribution. Insert a new result with exact hypotheses, parents, contribution and remaining boundaries.
Explore SampleWiki →03High-quality formal mathematicsFoundation
Build reusable probability, geometry, optimisation and sampling interfaces.
Current foundation. Lean declarations, the Registry and independent source review provide a formal foundation.
Next contribution. Stabilize missing shared lemmas with source fidelity and complete Lean proofs.
Inspect Lean declarations →04New principles and methodsResearch agenda
Cross-pollinate proof mechanisms across spaces, energies, divergences and dynamics.
Current foundation. The Functor Hypergraph records candidate mirrors with explicit hypothesis and failure maps.
Next contribution. Turn a candidate shared mechanism into a useful explanation, theorem or compiled transport adapter.
Explore the Functor Hypergraph →05Proof ablationResearch agenda
Keep the theorem fixed; test whether selected proof tools can be removed.
Current foundation. Statement seals, ingredient audits and encoder–denoiser review separate assumptions from proof machinery.
Next contribution. Declare forbidden inputs, find an alternative proof, and independently verify the same conclusion.
Inspect the verification workflow →06Theorem neighborhoodsResearch agenda
Vary a theorem's hypotheses and find what still holds, or exactly where it fails.
Current foundation. Typed theorem contracts, frontier cells and negative memory preserve the boundary of each route.
Next contribution. Test weaker curvature or regularity and approximate oracles with separate proofs or checked counterexamples.
Explore current frontiers →07Interpretable mathematical modelsResearch agenda
Make explanations, formal proofs and dependencies useful for specialized open mathematical tools.
Current foundation. Our aligned exposition, Lean interfaces and typed diagnostics provide inspectable material.
Next contribution. Prepare rights-cleared retrieval or model experiments. External references retain their license restrictions.
Open the research workspace →08Interactive mathematical teachingUnderstanding
Help students follow an idea from intuition through proof structure to Lean.
Current foundation. Textbook readers, learning paths and graph views offer different levels of mathematical detail.
Next contribution. Improve motivation, worked examples and navigation, then validate them with learners.
Start a learning path →09Model boundaries and failure modesResearch agenda
Make the assumptions behind mathematical guarantees available for application audits.
Current foundation. Explicit domains, regularity, oracle contracts and source audits expose where a guarantee applies.
Next contribution. Study discretization, finite precision, tails and model mismatch using formal counterexamples and application evidence.
Inspect analytic assumptions →From proof structure to reliable insight
A compressed graph keeps a path to the full proof. A conceptual mirror needs a proved adapter to become a formal edge. Encoder–denoiser review checks meaning; proof ablation additionally removes declared tools while preserving the theorem. Lean checks the stated model; applying it to reality also needs domain evidence.