论文库

原文摘要

Theoretical results in statistics and machine learning rest on long, technically delicate proofs, and fluent arguments generated by large language models are not necessarily correct. Automated formalization makes such arguments mechanically checkable, and automated proving goes further by discovering machine-checked proofs for statements whose proofs are incomplete or missing altogether. Both require reconstructing assumptions from source materials, accessing specialized mathematical infrastructure and managing long proof developments. We present Statopia, an ecosystem that jointly develops Statopia Prover, an independent agent specialized for formalizing and proving results in statistics and machine learning, and Statlib, a Lean~4 library built with the prover and organized for automated use. The prover controls its own execution without relying on external coding agents. It is built for formal proof discovery and checking existing proofs. A natural-language proof, when available, guides its search but is not required: from a statement alone, the prover develops the argument itself and constructs a Lean proof. Its workflow integrates source preparation, statement review, library supported planning and proof construction. Dynamic proof dependency graphs and task groups support parallel, resumable proof development. Statlib's shared definitions and theorem interfaces are organized for retrieval and composition by agents, and its coverage of statistics keeps expanding. Verified results and usage feedback from the prover inform reviewed library updates, so that proof development drives this expansion. A cross-platform application provides an interactive workspace for uploading source files and running tasks locally or in the cloud.