An Automated Theorem Proving System and Visualized Lean Library for Sampling Theory, Optimisation and Geometry

We present a theorem-proving harness and Samplinglib, a visualized Lean library for theorys of sampling, optimisation and geometry. The harness assigns bounded mathematical tasks to generalist workers, coordinates shared prerequisites, and separates Lean checking from source review. An encoder--decoder-inspired audit reconstructs a theorem from its Lean statement to expose changes in meaning. Samplinglib links six mathematical texts and a frontier literature index through shared formal foundations. Three views support source navigation, inspection of Lean declarations, and comparison of proof ideas. The Functor Hypergraph stores conditional mathematical correspondences with their assumptions, conclusions, sources, and evidence. Its purpose is to help agents recover useful mathematics and help readers understand how proofs connect. We describe the implementation, trace a shared strong-convexity proof and its reuse, and propose a longitudinal study of how persistent memory affects later work. The https://github.com/DakeBU/Automization-Sampling-Optimisation-Geometry-Lib and https://dakebu.github.io/Automization-Sampling-Optimisation-Geometry-Lib are publicly available.