StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean

# A Domain-Specific Benchmark for Stochastic Processes in Lean
Source: [https://arxiv.org/html/2609.09264](https://arxiv.org/html/2609.09264)
\\workshoptitle

The 6th Workshop on Mathematical Reasoning and AI

Debargha GangulyVikash SinghVipin ChaudharyAffiliation:Case Western Reserve UniversityAffiliation:\{idan, debargha, vikash, vipin\}@case\.eduAffiliation:[https://huggingface\.co/datasets/IdanDavidovich/StochBench](https://huggingface.co/datasets/IdanDavidovich/StochBench)

###### Abstract

Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field\-specific applications\. We introduceStochBench, a Lean 4 benchmark of 450 graduate stochastic\-processes problems at varying abstraction levels, each paired with its natural\-language source\. Addressing a field underrepresented in Mathlib, it covers finite and countable Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous\-time Markov processes\. Our Opus 4\.8\-based agent achieves a 34\.9% proof rate \(157/450\) under a 15\-minute per\-problem limit\.StochBenchbetter represents domain\-specific applied mathematics while remaining challenging for advanced provers\.

## 1Introduction

Lean enables machine\-checkable mathematics, with substantial formalizations including sphere packing in dimension eight, Brownian motion, and Fermat’s Last Theorem for regular primes\([Hariharan et al\., 2026](https://arxiv.org/html/2609.09264#bib.bib8);[Degenne et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib14);[Best et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib13)\)\. Extending this progress to everyday mathematical assistance requires evaluating how consistently automated provers handle a discipline’s recurring arguments\. Competition benchmarks and broad textbook collections offer valuable tests, but aggregate scores can obscure domain\-specific strengths and failures\([Zheng et al\., 2021](https://arxiv.org/html/2609.09264#bib.bib1);[Azerbayev et al\., 2023](https://arxiv.org/html/2609.09264#bib.bib2);[Tsoukalas et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib3)\)\.

We introduceStochBench, a Lean 4 benchmark for graduate stochastic processes, a field central to statistics and machine learning\. Concentrating on related problems in Markov chains, martingales, and continuous\-time processes, we prioritize within\-domain depth over cross\-domain breadth\. Some problems, however, require infrastructure unavailable in the Mathlib environment\([The mathlib Community, 2026](https://arxiv.org/html/2609.09264#bib.bib15)\)\.*Direct*targets use Mathlib or shared definitions, while*abstracted*targets take the required properties as hypotheses\. Lean verifies that each proved conclusion follows from its stated hypotheses\. We have taken utmost care to make sure the \(all human written\) definitions and hypotheses faithfully represent the source problem, but can benefit from further peer review\.

Our contributions are:

1. 1\.A domain\-focused benchmark\.We release 450 Lean 4 theorem targets paired with informal statements, alongside shared definitions and baseline proof attempts\.
2. 2\.A scope\-aware baseline evaluation\.We annotate formalization scope and evaluate a compiler\-guided proof agent under a 15\-minute per\-problem cap, reporting results by topic and representation\.

![Refer to caption](https://arxiv.org/html/2609.09264v1/Figure1.png)Figure 1:Construction ofStochBench: mathematician\-led curation and LLM\-assisted formalization with shared definitions produce 450 Lean 4 targets across eight topics, comprising 114 direct and 336 abstracted statements\.
## 2Related Work

Benchmarks for formal mathematical reasoning\.Lean\-based evaluation has developed along complementary axes of competition difficulty, curricular coverage, and research context\.miniF2F\([Zheng et al\., 2021](https://arxiv.org/html/2609.09264#bib.bib1)\)established a benchmark centered on Olympiad\-style mathematics,ProofNet\([Azerbayev et al\., 2023](https://arxiv.org/html/2609.09264#bib.bib2)\)paired informal statements and proofs with formal undergraduate theorem statements, andPutnamBench\([Tsoukalas et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib3)\)extended competition\-based evaluation to challenging undergraduate problems\.FormalMATH\([Yu et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib16)\)expanded the scale and disciplinary coverage of Lean 4 benchmarks, whileFormalProofBench\([Ravi et al\., 2026](https://arxiv.org/html/2609.09264#bib.bib4)\)targeted advanced undergraduate and graduate problems from textbooks and qualifying examinations\. Moving toward mathematical practice,RLMEval\([Poiroux et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib17)\)evaluates theorems from research\-level Lean formalization projects, andFormalML\([Yang et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib18)\)studies subgoal completion in machine\-learning theory, including optimization and probability inequalities\.

Proof automation, representation, and semantic faithfulness\.Lean 4\([Moura and Ullrich, 2021](https://arxiv.org/html/2609.09264#bib.bib5)\)and Mathlib\([The mathlib Community, 2020](https://arxiv.org/html/2609.09264#bib.bib19)\)provide an extensible proof environment and reusable mathematical abstractions for automated reasoning\.LeanDojo\([Yang et al\., 2023](https://arxiv.org/html/2609.09264#bib.bib20)\)combines programmatic proof interaction with retrieval\-augmented premise selection, whileLean Copilot\([Song et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib21)\)integrates tactic suggestion and proof search into interactive formalization\.Lean\-STaR\([Lin et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib22)\)interleaves informal reasoning with tactic generation;DeepSeek\-Prover\-V1\.5\([Xin et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib23)\)combines proof\-assistant feedback with reinforcement learning and tree search; andDeepSeek\-Prover\-V2\([Ren et al\., 2025](https://arxiv.org/html/2609.09264#bib.bib24)\)develops reinforcement learning around subgoal decomposition\. These advances address proof construction, but successful checking alone does not establish correspondence with an intended informal claim\.FormalAlign\([Lu et al\., 2024](https://arxiv.org/html/2609.09264#bib.bib25)\)explicitly evaluates informal–formal semantic alignment, whileMathAtlas\([Patel et al\., 2026](https://arxiv.org/html/2609.09264#bib.bib26)\)examines graduate\-level autoformalization with definitions and dependency structure\.TaoBench\([Taylor et al\., 2026](https://arxiv.org/html/2609.09264#bib.bib27)\)isolates a related representation issue through paired, mathematically equivalent statements expressed using bespoke and Mathlib definitions\.

Formal probability and stochastic\-process infrastructure\.Substantial Lean developments already support the mathematics underlyingStochBench\.[Ying and Degenne \(2022\)](https://arxiv.org/html/2609.09264#bib.bib28)formalize Doob’s martingale convergence theorems together with conditional expectation, stopping times, and martingale theory;[Marion \(2025\)](https://arxiv.org/html/2609.09264#bib.bib29)constructs trajectory\-space probability measures through the Ionescu–Tulcea theorem, and[Degenne \(2025\)](https://arxiv.org/html/2609.09264#bib.bib30)develops Markov kernels and disintegration\.[Degenne et al\. \(2025\)](https://arxiv.org/html/2609.09264#bib.bib14)formalize Brownian motion and its extension and path\-continuity machinery, while[Coelho \(2026b\)](https://arxiv.org/html/2609.09264#bib.bib31)develops theL2L^\{2\}Itô integral and Itô’s formula forC3C^\{3\}functions with bounded derivatives\. Complementary work connects textbook probability to Mathlib interfaces\([Deng and Shum, 2026](https://arxiv.org/html/2609.09264#bib.bib32)\), verifies reinforcement\-learning convergence\([Zhang, 2025](https://arxiv.org/html/2609.09264#bib.bib33)\), and constructs a mathematical\-finance library with explicit faithfulness auditing\([Coelho, 2026a](https://arxiv.org/html/2609.09264#bib.bib34)\)\.

## 3TheStochBenchBenchmark

#### Sources and selection\.

StochBenchcontains 450 Lean 4 theorem targets in graduate stochastic processes\. We combine problems written for the benchmark with exercises, lemmas, theorems, and corollaries selected from*Probability, Mathematical Statistics, and Stochastic Processes*\([Siegrist, 2022](https://arxiv.org/html/2609.09264#bib.bib12)\)and the MIT course notes and assignments for*Introduction to Stochastic Processes*\([Wu, 2015](https://arxiv.org/html/2609.09264#bib.bib9)\),*Advanced Stochastic Processes*\([Gamarnik, 2013](https://arxiv.org/html/2609.09264#bib.bib10)\), and*Discrete Stochastic Processes*\([Gallager, 2011](https://arxiv.org/html/2609.09264#bib.bib11)\)\. We selected problems for their relevance to stochastic processes and wrote them as claims with hypotheses\. Statements that are closer to general probability theory, such as “show that the total variation distance satisfies triangle inequality :‖μ−ν‖T​V≤‖μ−η‖T​V\+\|\|η−ν\|\|T​V\|\|\\mu\-\\nu\|\|\_\{TV\}\\leq\|\|\\mu\-\\eta\|\|\_\{TV\}\+\|\|\\eta\-\\nu\|\|\_\{TV\}”, were not included\. The corpus covers eight topics, summarized in Table[1](https://arxiv.org/html/2609.09264#S3.T1)\.

#### Statement construction\.

All benchmark\-specific definitions, hypotheses and questions are human\-written\. An Opus 4\.8\-based formalizer assisted with expressing the problems as Lean theorem statements\. We revised candidate statements using Lean feedback until they elaborated in Lean 4\.30\.0 with a fixed Mathlib version\. Elaboration checks that a statement is well\-typed\. We consider the task to prove the theorem with established correspondence with the source problem\. On the off chance that a formalization error has crept in, we also accept a kernel\-checked proof of the theorem being incorrect\.

#### Shared mathematical definitions\.

We build shared abstractions and definitions for recurring concepts\. Finite\-state chains use a common matrix representation for stochasticity, stationarity, irreducibility, aperiodicity, eventual positivity of transition powers, detailed balance, time reversal, and total\-variation distance\.IsHittingSolutionandreturnTimeexpress first\-step equations, whilenstepdefines transition powers through infinite sums for countable\-state formulations\. Other definitions connect the targets to Mathlib:natStopconverts natural\-valued stopping times toWithTop,runningMaxexpresses finite running maxima, andIsConstDriftstates conditional increment identities\. Reusing these definitions gives related targets a common mathematical representation\.

#### Marginals and joint process laws\.

We distinguish the distribution of a process at one time from its joint behavior over time\.HasMatrixMarginalsrelates the distribution ofXnX\_\{n\}to the corresponding row ofPnP^\{n\}\.HasChainLawinstead specifies finite\-dimensional probabilities through

ℙμ​\(X0=x0,…,Xn=xn\)=ν⁡\(x0\)​∏i=0n−1P⁡\(xi,xi\+1\)\.\\mathbb\{P\}\_\{\\mu\}\(X\_\{0\}=x\_\{0\},\\ldots,X\_\{n\}=x\_\{n\}\)=\\nu\(x\_\{0\}\)\\prod\_\{i=0\}^\{n\-1\}P\(x\_\{i\},x\_\{i\+1\}\)\.The coupling\-bound target combines matrix marginals with an explicit condition that the processes agree after the meeting time\. The strong\-stationary\-time target uses the joint law and stopping\-time conditions to relate the state at the stopping time to the state at a later deterministic time\. These representations specify which information about the process is available to the prover\.

Formalization scope\.Some problems require infrastructure unavailable in the Mathlib environment\.*Direct*targets use Mathlib objects or shared definitions, while*abstracted*targets take the required properties as hypotheses\. The JSON records these labels asliteralandabstract, respectively\. The supplied properties may define an object or provide intermediate results from the source problem\. These are different choices: specifying Brownian\-motion properties does not assume a quadratic\-variation conclusion, whereas assuming memorylessness removes the need to derive it from continuous\-time chain dynamics\. Likewise, a hitting\-time target stated through first\-step equations need not establish that their solution equals a pathwise expected hitting time\.

Path properties and convergence\.The targets state the required form of convergence explicitly\. Brownian\-motion properties are expressed through Gaussian increment laws, independence, and almost\-sure path continuity; several targets package these properties in a localIsBMdefinition\. The quadratic\-variation target asks for convergence of the mean\-square error as the partition mesh tends to zero\. The Donsker target asks for convergence of expectations for every bounded continuous functional onC⁡\(\[0,T\],ℝ\)C\(\[0,T\],\\mathbb\{R\}\), rather than only convergence at individual times\. A separate target asks for existence and uniqueness of Wiener measure on continuous path space\.

Human review and release\.We reviewed the definitions and hypotheses against the source problems, but they would benefit from further peer review\. Lean verifies that each completed proof establishes its conclusion under the stated hypotheses; source review assesses whether the definitions and hypotheses represent the intended problem\. Each JSON record contains an identifier, a problem name, an informal statement, a Lean target, and a representation label\. We also release the shared definitions and baseline proof attempts\. The release is a collection of theorem targets, not a claim that all targets have complete proofs\. Baseline proof checking and results are described in Section[4](https://arxiv.org/html/2609.09264#S4)\.

Table 1:Corpus composition and baseline results forStochBench\(recorded proving time at most 15 minutes\)\. Only proofs with recorded proving times of at most 900 seconds are counted\. Topic rates use all items in the topic; class rates use all items in the class\. The class comparison is descriptive, not a controlled causal effect\.

## 4Evaluation

We evaluated a multi\-turn tool\-using Opus 4\.8\-based agent usinglean4skillsand the Lean LSP MCP server\([Freer, 2025](https://arxiv.org/html/2609.09264#bib.bib7);[Dressler, 2025](https://arxiv.org/html/2609.09264#bib.bib6)\)\. Each target received one run capped at 15 minutes, allowing Lean\-error inspection, library and shared\-definition search,loogleandleansearchqueries, and proof revisions\. The same model family assisted with statement construction\. This is a single\-agent, single\-budget baseline, not a model comparison or repeated\-run evaluation\.

The agent produced 157 clean proofs out of 450\. A proof is*clean*if Lean accepts it withoutsorry,sorryAx, or additional admitted facts, checked by Lean comparator\. Tables[1](https://arxiv.org/html/2609.09264#S3.T1)and[1](https://arxiv.org/html/2609.09264#S3.T1)report topic and class breakdowns\. These are descriptive comparisons: they do not separate abstraction effects from differences in problems or library support\.

Qualitative inspection found proof\-search failures on plausible targets, missing lemmas or difficult library interfaces, and a smaller group of formalization defects, including missing measurability, integrability, or non\-emptiness assumptions\.

## 5Limitations and Conclusion

We note thatStochBench’s question curation, faithfulness review, and its topic and direct/abstracted classifications are currently decided by human curators, introducing some bias; as the corresponding terminologies were not rigorously defined within the scope of this work\. Despite these limitations,StochBenchprovides a focused testbed for evaluating proof agents on graduate stochastic processes\. Its newly constructed informal–formal pairs can support autoformalization training, while successfully checked baseline proofs provide supervision for proof generation\. Together with the shared definitions, these resources support both the development of stronger domain\-specific provers and the continued formalization of stochastic processes in Lean\.

## References

- Azerbayevet al\.\(2023\)Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. AvigadProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.arXiv\.org\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2302.12433)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1),[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Bestet al\.\(2025\)A\. Best, C\. Birkbeck, R\. Brasca, E\. R\. Boidi, R\. van De Velde, and A\. YangA complete formalization of fermat’s last theorem for regular primes in lean\.External Links:2410\.01466,[Link](https://arxiv.org/abs/2410.01466)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1)\.
- Coelho \(2026a\)R\. CoelhoA Formally Verified Library of Mathematical Finance in Lean 4\.External Links:2606\.01356,[Document](https://dx.doi.org/10.48550/arXiv.2606.01356),[Link](https://arxiv.org/abs/2606.01356)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Coelho \(2026b\)R\. CoelhoA Machine\-Checked Itô Calculus for Brownian Motion\.External Links:2606\.15089,[Document](https://dx.doi.org/10.48550/arXiv.2606.15089),[Link](https://arxiv.org/abs/2606.15089)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Degenneet al\.\(2025\)R\. Degenne, D\. Ledvinka, E\. Marion, and P\. PfaffelhuberFormalization of brownian motion in lean\.External Links:2511\.20118,[Link](https://arxiv.org/abs/2511.20118)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1),[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Degenne \(2025\)R\. DegenneMarkov Kernels in Mathlib’s Probability Library\.External Links:2510\.04070,[Document](https://dx.doi.org/10.48550/arXiv.2510.04070),[Link](https://arxiv.org/abs/2510.04070)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Deng and Shum \(2026\)S\. Deng and K\. W\. ShumFrom Lecture Notes to Lean: Formalizing a Textbook on Probability Theory\.External Links:2607\.27298,[Document](https://dx.doi.org/10.48550/arXiv.2607.27298),[Link](https://arxiv.org/abs/2607.27298)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Dressler \(2025\)Lean LSP MCP: Tools for agentic interaction with the Lean theorem proverExternal Links:[Link](https://github.com/oOo0oOo/lean-lsp-mcp)Cited by:[§4](https://arxiv.org/html/2609.09264#S4.p1.1)\.
- Freer \(2025\)Lean 4 Skills: theorem proving skill and workflow pack for AI coding agentsExternal Links:[Link](https://github.com/cameronfreer/lean4-skills)Cited by:[§4](https://arxiv.org/html/2609.09264#S4.p1.1)\.
- Gallager \(2011\)R\. Gallager6\.262 Discrete Stochastic Processes\.Note:Spring 2011\. Massachusetts Institute of Technology: MIT OpenCourseWare,[https://ocw\.mit\.edu/](https://ocw.mit.edu/)License: Creative Commons BY\-NC\-SACited by:[§3](https://arxiv.org/html/2609.09264#S3.SS0.SSS0.Px1.p1.1)\.
- Gamarnik \(2013\)D\. Gamarnik15\.070J Advanced Stochastic Processes\.Note:Fall 2013\. Massachusetts Institute of Technology: MIT OpenCourseWare,[https://ocw\.mit\.edu/](https://ocw.mit.edu/)License: Creative Commons BY\-NC\-SACited by:[§3](https://arxiv.org/html/2609.09264#S3.SS0.SSS0.Px1.p1.1)\.
- Hariharanet al\.\(2026\)S\. Hariharan, C\. Birkbeck, S\. Lee, H\. K\. G\. Ma, B\. Mehta, A\. Poiroux, and M\. ViazovskaA milestone in formalization: the sphere packing problem in dimension 8\.External Links:2604\.23468,[Link](https://arxiv.org/abs/2604.23468)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1)\.
- Linet al\.\(2024\)H\. Lin, Z\. Sun, Y\. Yang, and S\. WelleckLean\-STaR: Learning to Interleave Thinking and Proving\.External Links:2407\.10040,[Document](https://dx.doi.org/10.48550/arXiv.2407.10040),[Link](https://arxiv.org/abs/2407.10040)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Luet al\.\(2024\)J\. Lu, Y\. Wan, Y\. Huang, J\. Xiong, Z\. Liu, and Z\. GuoFormalAlign: Automated Alignment Evaluation for Autoformalization\.External Links:2410\.10135,[Document](https://dx.doi.org/10.48550/arXiv.2410.10135),[Link](https://arxiv.org/abs/2410.10135)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Marion \(2025\)E\. MarionA Formalization of the Ionescu\-Tulcea Theorem in Mathlib\.External Links:2506\.18616,[Document](https://dx.doi.org/10.48550/arXiv.2506.18616),[Link](https://arxiv.org/abs/2506.18616)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Moura and Ullrich \(2021\)L\. D\. Moura and S\. UllrichThe Lean 4 theorem prover and programming language\.InCADE,pp\. 625–635\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Patelet al\.\(2026\)N\. Patel, N\. Arias, D\. Babayan, V\. Cochran, T\. Libman, H\. Mahmood, L\. McCarty, S\. Munoz, L\. Willey, and J\. FlaniganMathAtlas: A Benchmark for Autoformalization in the Wild\.External Links:2605\.14061,[Document](https://dx.doi.org/10.48550/arXiv.2605.14061),[Link](https://arxiv.org/abs/2605.14061)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Poirouxet al\.\(2025\)A\. Poiroux, A\. Bosselut, and V\. KunčakRLMEval: Evaluating Research\-Level Neural Theorem Proving\.External Links:2510\.25427,[Document](https://dx.doi.org/10.48550/arXiv.2510.25427),[Link](https://arxiv.org/abs/2510.25427)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Raviet al\.\(2026\)N\. Ravi, K\. Ying, V\. Nesterov, R\. Krishnan, E\. Uskuplu, B\. Xia, J\. Aswedige, and L\. NasholdFormalProofBench: can models write graduate level math proofs that are formally verified?\.arXiv\.org\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2603.26996)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Renet al\.\(2025\)Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. RuanDeepSeek\-Prover\-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition\.External Links:2504\.21801,[Document](https://dx.doi.org/10.48550/arXiv.2504.21801),[Link](https://arxiv.org/abs/2504.21801)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Siegrist \(2022\)K\. SiegristProbability, Mathematical Statistics, and Stochastic Processes\.Note:LibreTextsOriginally sourced from[http://www\.randomservices\.org/random](http://www.randomservices.org/random)\. License: CC BY 2\.0External Links:[Link](https://stats.libretexts.org/Bookshelves/Probability_Theory/Probability_Mathematical_Statistics_and_Stochastic_Processes_(Siegrist))Cited by:[§3](https://arxiv.org/html/2609.09264#S3.SS0.SSS0.Px1.p1.1)\.
- Songet al\.\(2024\)P\. Song, K\. Yang, and A\. AnandkumarTowards Large Language Models as Copilots for Theorem Proving in Lean\.External Links:2404\.12534,[Document](https://dx.doi.org/10.48550/arXiv.2404.12534),[Link](https://arxiv.org/abs/2404.12534)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Tayloret al\.\(2026\)A\. K\. Taylor, J\. Zhang, E\. Ji, V\. Sahai, H\. Deng, Y\. Chen, Y\. Yuan, D\. Wu, J\. Gu, K\. Chang, N\. Peng, A\. Sahai, and W\. WangTaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?\.External Links:2603\.12744,[Document](https://dx.doi.org/10.48550/arXiv.2603.12744),[Link](https://arxiv.org/abs/2603.12744)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- The mathlib Community \(2020\)The mathlib CommunityThe Lean Mathematical Library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,pp\. 367–381\.External Links:[Document](https://dx.doi.org/10.1145/3372885.3373824),[Link](https://doi.org/10.1145/3372885.3373824)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- The mathlib Community \(2026\)The mathlib CommunityMissing undergraduate mathematics in mathlib\.Note:[https://leanprover\-community\.github\.io/undergrad\_todo\.html](https://leanprover-community.github.io/undergrad_todo.html)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p2.1)\.
- Tsoukalaset al\.\(2024\)G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. ChaudhuriPutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.Advances in Neural Information Processing Systems 37,pp\. 11545–11569\.External Links:[Document](https://dx.doi.org/10.52202/079017-0368)Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1),[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Wu \(2015\)H\. Wu18\.445 Introduction to Stochastic Processes\.Note:Spring 2015\. Massachusetts Institute of Technology: MIT OpenCourseWare,[https://ocw\.mit\.edu/](https://ocw.mit.edu/)License: Creative Commons BY\-NC\-SACited by:[§3](https://arxiv.org/html/2609.09264#S3.SS0.SSS0.Px1.p1.1)\.
- Xinet al\.\(2024\)H\. Xin, Z\. Z\. Ren, J\. Song, Z\. Shao, W\. Zhao, H\. Wang, B\. Liu, L\. Zhang, X\. Lu, Q\. Du, W\. Gao, Q\. Zhu, D\. Yang, Z\. Gou, Z\. F\. Wu, F\. Luo, and C\. RuanDeepSeek\-Prover\-V1\.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte\-Carlo Tree Search\.External Links:2408\.08152,[Document](https://dx.doi.org/10.48550/arXiv.2408.08152),[Link](https://arxiv.org/abs/2408.08152)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Yanget al\.\(2023\)K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. AnandkumarLeanDojo: Theorem Proving with Retrieval\-Augmented Language Models\.External Links:2306\.15626,[Document](https://dx.doi.org/10.48550/arXiv.2306.15626),[Link](https://arxiv.org/abs/2306.15626)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p2.1)\.
- Yanget al\.\(2025\)X\. Yang, Z\. Zhang, J\. Cao, Z\. Zhou, Z\. Li, L\. Guo, Y\. Yao, T\. Chen, Y\. Li, and X\. MaFormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory\.External Links:2510\.02335,[Document](https://dx.doi.org/10.48550/arXiv.2510.02335),[Link](https://arxiv.org/abs/2510.02335)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Ying and Degenne \(2022\)K\. Ying and R\. DegenneA Formalization of Doob’s Martingale Convergence Theorems in mathlib\.External Links:2212\.05578,[Document](https://dx.doi.org/10.48550/arXiv.2212.05578),[Link](https://arxiv.org/abs/2212.05578)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Yuet al\.\(2025\)Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Z\. Yuan, H\. Xin, W\. Huang, Y\. Wen, G\. Zhang, and W\. LiuFormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models\.External Links:2505\.02735,[Document](https://dx.doi.org/10.48550/arXiv.2505.02735),[Link](https://arxiv.org/abs/2505.02735)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.
- Zhang \(2025\)S\. ZhangTowards Formalizing Reinforcement Learning Theory: A Robbins\-Siegmund Approach\.External Links:2511\.03618,[Document](https://dx.doi.org/10.48550/arXiv.2511.03618),[Link](https://arxiv.org/abs/2511.03618)Cited by:[§2](https://arxiv.org/html/2609.09264#S2.p3.1)\.
- Zhenget al\.\(2021\)K\. Zheng, J\. M\. Han, and S\. PoluminiF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2609.09264#S1.p1.1),[§2](https://arxiv.org/html/2609.09264#S2.p1.1)\.

## Appendix ASupplementary material

### A\.1An abstracted proof example \- SOTA Prover

We illustrate Q361 through its natural\-language statement, Lean abstraction, and an agent\-generated proof obtained in a separate run lasting more than 30 minutes, outside the 15\-minute baseline protocol\.

#### Natural\-language statement\.

Suppose that a Markov chain on a finite, nonempty state spaceΩ\\Omegais irreducible and has stationary probability measureπ\\pi\. Define the hitting time ofx∈Ωx\\in\\Omegaby

τx=min⁡\{n≥0:Xn=x\}\.\\tau\_\{x\}=\\min\\\{n\\geq 0:X\_\{n\}=x\\\}\.For a fixed statea∈Ωa\\in\\Omega, let

t⊙=∑x∈Ω𝔼a​\[τx\]​π​\(x\),thit=maxx,y∈Ω⁡𝔼x​\[τy\]≥t⊙\.t\_\{\\odot\}=\\sum\_\{x\\in\\Omega\}\\mathbb\{E\}\_\{a\}\[\\tau\_\{x\}\]\\,\\pi\(x\),\\qquad t\_\{\\mathrm\{hit\}\}=\\max\_\{x,y\\in\\Omega\}\\mathbb\{E\}\_\{x\}\[\\tau\_\{y\}\]\\geq t\_\{\\odot\}\.Show that

thit≤2​maxw∈Ω​𝔼π​\[τw\],𝔼π​\[τw\]=∑x∈Ωπ⁡\(x\)​𝔼x​\[τw\]\.t\_\{\\mathrm\{hit\}\}\\leq 2\\max\_\{w\\in\\Omega\}\\mathbb\{E\}\_\{\\pi\}\[\\tau\_\{w\}\],\\qquad\\mathbb\{E\}\_\{\\pi\}\[\\tau\_\{w\}\]=\\sum\_\{x\\in\\Omega\}\\pi\(x\)\\mathbb\{E\}\_\{x\}\[\\tau\_\{w\}\]\.

#### Formalization\.

The Lean statement represents expected hitting times by a real\-valued functiong⁡\(x,y\)g\(x,y\)satisfying the first\-step equations

g⁡\(x,y\)=\{0,x=y,1\+∑z∈ΩP⁡\(x,z\)​g​\(z,y\),x≠y\.g\(x,y\)=\\begin\{cases\}0,&x=y,\\\\ 1\+\\sum\_\{z\\in\\Omega\}P\(x,z\)g\(z,y\),&x\\neq y\.\\end\{cases\}These equations are supplied byIsHittingSolution; the proof works with this characterization rather than constructing hitting\-time random variables\. The assumptionsIsStochastic,IsIrreducible, andIsStationaryspecify the transition matrix and stationary distribution\. The auxiliary quantityt⊙t\_\{\\odot\}and the given lower bound onthitt\_\{\\mathrm\{hit\}\}are not needed for the formalized conclusion\.

#### Proof structure and difficulty\.

Although Q361 asks for a single inequality, the generated proof develops nine auxiliary theorems across several levels of abstraction\. It establishes nonnegativity of matrix powers and hitting\-time solutions, extends closure under positive one\-step transitions to positive matrix powers, and proves a maximum\-principle propagation lemma\. A return\-time identity yields harmonicity of Kemeny’s functionK⁡\(x\)=∑yπ⁡\(y\)​g​\(x,y\)K\(x\)=\\sum\_\{y\}\\pi\(y\)g\(x,y\), whose constancy follows from irreducibility and the maximum principle\. The same propagation lemmas are reused forθ⁡\(x\)=g⁡\(x,b\)−g⁡\(x,c\)\\theta\(x\)=g\(x,b\)\-g\(x,c\)to establish the hitting\-time triangle inequality\. Stationary averaging then combines these results into a pointwise bound, which is lifted to the required supremum inequality\.

#### Implications for proof search\.

The abstraction supplies the first\-step equations, not Kemeny constancy or the triangle inequality\. The proof therefore builds supporting mathematics rather than merely simplifying the supplied hypotheses\. Its structure illustrates a challenge for hierarchical proof search: identifying useful intermediate statements, proving them at sufficient generality for reuse, and coordinating their dependencies\. Here, elementary matrix and finite\-sum reasoning supports harmonic\-function arguments, which in turn support the global hitting\-time bound\. The agent\-produced result is thus a coherent collection of auxiliary theorems together with their final composition\. This example shows how an abstracted benchmark target can test mathematical proof construction beyond local tactic selection\.

importMathlib

importLeanproj\.Basic

openMeasureTheoryProbabilityTheoryFilterAuto

openscopedENNRealNNRealTopologyMatrixRealInnerProductSpace

attribute\[localinstance\]Classical\.propDecidable

set\_optionmaxHeartbeats2000000

set\_optionmaxRecDepth4096

namespaceQ361Helpers

openFinset

theorempow\_nonneg\_entry\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\):∀\\forallnxy,0≤\\leq\(P^n\)xy:=by

intron

inductionnwith

\|zero=\>introxy;simp\[pow\_zero,Matrix\.one\_apply\];split<;\>norm\_num

\|succkih=\>

introxy

rw\[pow\_succ,Matrix\.mul\_apply\]

applyFinset\.sum\_nonneg;introz\_

exactmul\_nonneg\(ihxz\)\(hP1zy\)

theoremg\_nonneg\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hg:∀\\forallxy,gxy=ifx=ythen0else1\+∑\\sumz,Pxz\*gzy\)

\(y:Ω\\Omega\):∀\\forallx,0≤\\leqgxy:=by

obtain⟨\\langlex0,\-,hx0⟩\\rangle:=Finset\.exists\_min\_imageFinset\.univ\(funx=\>gxy\)

⟨\\langleClassical\.arbitraryΩ\\Omega,Finset\.mem\_univ\_⟩\\rangle

havehmin:∀\\forallx,gx0y≤\\leqgxy:=funx=\>hx0x\(Finset\.mem\_univx\)

havehx0y:gx0y=0:=by

by\_casesh:x0=y

⋅\\cdotrw\[hgx0y,if\_posh\]

⋅\\cdotexfalso

havehval:=hgx0y

rw\[if\_negh\]athval

havehlb:\(1:ℝ\\mathbb\{R\}\)\+∑\\sumz,Px0z\*gzy≥\\geq1\+∑\\sumz,Px0z\*gx0y:=by

have:\(∑\\sumz,Px0z\*gzy\)≥\\geq∑\\sumz,Px0z\*gx0y:=by

applyFinset\.sum\_le\_sum;introz\_

exactmul\_le\_mul\_of\_nonneg\_left\(hminz\)\(hP1x0z\)

linarith

havehsum:\(∑\\sumz,Px0z\*gx0y\)=gx0y:=by

rw\[←\\leftarrowFinset\.sum\_mul,hP2x0,one\_mul\]

rw\[hsum\]athlb

linarith\[hval,hlb\]

introx

calc0=gx0y:=hx0y\.symm

\_≤\\leqgxy:=hminx

closedunderpositive‘n‘\-steptransitions\.\-/

theoremreach\_closed\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)

\(A:Ω\\Omega→\\rightarrowProp\)\(hclosed:∀\\forallx,Ax→\\rightarrow∀\\forallz,0<Pxz→\\rightarrowAz\)

\(x0:Ω\\Omega\)\(hx0:Ax0\):∀\\forallnz,0<\(P^n\)x0z→\\rightarrowAz:=by

havehpow:=pow\_nonneg\_entryPhP1

intron

inductionnwith

\|zero=\>

introzhz

rw\[pow\_zero,Matrix\.one\_apply\]athz

by\_casesh:x0=z

⋅\\cdotrwa\[←\\leftarrowh\]

⋅\\cdotsimp\[h\]athz

\|succkih=\>

introzhz

rw\[pow\_succ,Matrix\.mul\_apply\]athz

havehex:∃\\existsw∈\\inFinset\.univ,\(0:ℝ\\mathbb\{R\}\)<\(P^k\)x0w\*Pwz:=by

applyFinset\.exists\_lt\_of\_sum\_lt;simpausinghz

obtain⟨\\langlew,\-,hw⟩\\rangle:=hex

haveh1:0<\(P^k\)x0w:=

lt\_of\_le\_of\_ne\(hpowkx0w\)\(funh=\>byrw\[←\\leftarrowh,zero\_mul\]athw;exactlt\_irrefl\_hw\)

haveh2:0<Pwz:=

lt\_of\_le\_of\_ne\(hP1wz\)\(funh=\>byrw\[←\\leftarrowh,mul\_zero\]athw;exactlt\_irrefl\_hw\)

exacthclosedw\(ihwh1\)zh2

positively\-reachableneighboursalsoattainthemaximum\.\-/

theoremprop\_step\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(f:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(m:ℝ\\mathbb\{R\}\)\(hmax:∀\\forallz,fz≤\\leqm\)\(x:Ω\\Omega\)\(hfx:fx=m\)

\(hharm:fx=∑\\sumz,Pxz\*fz\)\(z:Ω\\Omega\)\(hz:0<Pxz\):fz=m:=by

havehsum0:\(∑\\sumw,Pxw\*\(m\-fw\)\)=0:=by

have:\(∑\\sumw,Pxw\*\(m\-fw\)\)=\(∑\\sumw,Pxw\)\*m\-∑\\sumw,Pxw\*fw:=by

rw\[Finset\.sum\_mul,←\\leftarrowFinset\.sum\_sub\_distrib\]

applyFinset\.sum\_congrrfl;introw\_;ring

rw\[this,hP2x,one\_mul,←\\leftarrowhharm,hfx\];ring

havehnonneg:∀\\forallw∈\\inFinset\.univ,0≤\\leqPxw\*\(m\-fw\):=by

introw\_;exactmul\_nonneg\(hP1xw\)\(bylinarith\[hmaxw\]\)

havehzero:=\(Finset\.sum\_eq\_zero\_iff\_of\_nonneghnonneg\)\.mphsum0z\(Finset\.mem\_univz\)

have:m\-fz=0:=by

rcasesmul\_eq\_zero\.mphzerowithh\|h

⋅\\cdotlinarith\[hz\]

⋅\\cdotexacth

linarith

theoremreturnTime\_identity\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)

\(hg:∀\\forallxy,gxy=ifx=ythen0else1\+∑\\sumz,Pxz\*gzy\)

\(π\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hpi2:∑\\sumx,π\\pix=1\)

\(hpi3:∀\\forally,∑\\sumx,π\\pix\*Pxy=π\\piy\)\(w:Ω\\Omega\):

π\\piw\*\(1\+∑\\sumz,Pwz\*gzw\)=1:=by

havehswap:\(∑\\sumx,π\\pix\*∑\\sumz,Pxz\*gzw\)=∑\\sumx,π\\pix\*gxw:=by

havee1:\(∑\\sumx,π\\pix\*∑\\sumz,Pxz\*gzw\)=∑\\sumx,∑\\sumz,π\\pix\*\(Pxz\*gzw\):=by

applyFinset\.sum\_congrrfl;introx\_;rw\[Finset\.mul\_sum\]

rw\[e1,Finset\.sum\_comm\]

applyFinset\.sum\_congrrfl;introz\_

have:\(∑\\sumx,π\\pix\*\(Pxz\*gzw\)\)=\(∑\\sumx,π\\pix\*Pxz\)\*gzw:=by

rw\[Finset\.sum\_mul\];applyFinset\.sum\_congrrfl;introx\_;ring

rw\[this,hpi3z\]

haves1:\(∑\\sumx,ifx=wthen0elseπ\\pix\)=1\-π\\piw:=by

have:\(∑\\sumx,ifx=wthen0elseπ\\pix\)=∑\\sumx,\(π\\pix\-ifx=wthenπ\\pixelse0\):=by

applyFinset\.sum\_congrrfl;introx\_;by\_caseshx:x=w<;\>simp\[hx\]

rw\[this,Finset\.sum\_sub\_distrib,hpi2,Finset\.sum\_ite\_eq’Finset\.univwπ\\pi\];simp

haves2:\(∑\\sumx,ifx=wthen0elseπ\\pix\*∑\\sumz,Pxz\*gzw\)

=\(∑\\sumx,π\\pix\*gxw\)\-π\\piw\*∑\\sumz,Pwz\*gzw:=by

havestep1:\(∑\\sumx,ifx=wthen0elseπ\\pix\*∑\\sumz,Pxz\*gzw\)

=\(∑\\sumx,π\\pix\*∑\\sumz,Pxz\*gzw\)\-π\\piw\*∑\\sumz,Pwz\*gzw:=by

have:\(∑\\sumx,ifx=wthen0elseπ\\pix\*∑\\sumz,Pxz\*gzw\)

=∑\\sumx,\(\(π\\pix\*∑\\sumz,Pxz\*gzw\)

\-\(ifx=wthenπ\\piw\*∑\\sumz,Pwz\*gzwelse0\)\):=by

applyFinset\.sum\_congrrfl;introx\_;by\_caseshx:x=w<;\>simp\[hx\]

rw\[this,Finset\.sum\_sub\_distrib,Finset\.sum\_ite\_eq’Finset\.univw\];simp

rw\[step1,hswap\]

havekey:\(∑\\sumx,π\\pix\*gxw\)

=\(1\-π\\piw\)\+\(\(∑\\sumx,π\\pix\*gxw\)\-π\\piw\*\(∑\\sumz,Pwz\*gzw\)\):=by

havee1:\(∑\\sumx,π\\pix\*gxw\)

=∑\\sumx,π\\pix\*\(ifx=wthen0else1\+∑\\sumz,Pxz\*gzw\):=by

applyFinset\.sum\_congrrfl;introx\_;rw\[hgxw\]

havee2:\(∑\\sumx,π\\pix\*\(ifx=wthen0else1\+∑\\sumz,Pxz\*gzw\)\)

=\(∑\\sumx,ifx=wthen0elseπ\\pix\)

\+\(∑\\sumx,ifx=wthen0elseπ\\pix\*∑\\sumz,Pxz\*gzw\):=by

rw\[←\\leftarrowFinset\.sum\_add\_distrib\]

applyFinset\.sum\_congrrfl;introx\_

by\_caseshx:x=w<;\>simp\[hx\]<;\>ring

conv\_lhs=\>rw\[e1,e2,s1,s2\]

nlinarith\[key\]

theoremK\_harmonic\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hg:∀\\forallxy,gxy=ifx=ythen0else1\+∑\\sumz,Pxz\*gzy\)

\(π\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hpi1:∀\\forallx,0≤\\leqπ\\pix\)\(hpi2:∑\\sumx,π\\pix=1\)

\(hRT:∀\\forallw,π\\piw\*\(1\+∑\\sumz,Pwz\*gzw\)=1\)\(x:Ω\\Omega\):

\(∑\\sumc,π\\pic\*gxc\)=∑\\sumz,Pxz\*\(∑\\sumc,π\\pic\*gzc\):=by

havehpx:π\\pix\*\(1\+∑\\sumz,Pxz\*gzx\)=1:=hRTx

havehpxpos:0<π\\pix:=by

rcases\(hpi1x\)\.lt\_or\_eqwithh\|h

⋅\\cdotexacth

⋅\\cdotexfalso;rw\[←\\leftarrowh,zero\_mul\]athpx;norm\_numathpx

havehret:π\\pix\*\(∑\\sumz,Pxz\*gzx\)=1\-π\\pix:=bynlinarith\[hpx\]

havee1:\(∑\\sumc,π\\pic\*gxc\)=∑\\sumc,\(ifc=xthen0elseπ\\pic\*\(1\+∑\\sumz,Pxz\*gzc\)\):=by

applyFinset\.sum\_congrrfl;introc\_

rw\[hgxc\];by\_casesh:x=c

⋅\\cdotsimp\[h\]

⋅\\cdotrw\[if\_negh,if\_neg\(Ne\.symmh\)\]

havee2:\(∑\\sumc,\(ifc=xthen0elseπ\\pic\*\(1\+∑\\sumz,Pxz\*gzc\)\)\)

=\(∑\\sumc,ifc=xthen0elseπ\\pic\)

\+\(∑\\sumc,ifc=xthen0elseπ\\pic\*∑\\sumz,Pxz\*gzc\):=by

rw\[←\\leftarrowFinset\.sum\_add\_distrib\];applyFinset\.sum\_congrrfl;introc\_

by\_casesh:c=x<;\>simp\[h\]<;\>ring

havesa:\(∑\\sumc,ifc=xthen0elseπ\\pic\)=1\-π\\pix:=by

have:\(∑\\sumc,ifc=xthen0elseπ\\pic\)=∑\\sumc,\(π\\pic\-ifc=xthenπ\\picelse0\):=by

applyFinset\.sum\_congrrfl;introc\_;by\_casesh:c=x<;\>simp\[h\]

rw\[this,Finset\.sum\_sub\_distrib,hpi2,Finset\.sum\_ite\_eq’Finset\.univxπ\\pi\];simp

havesb:\(∑\\sumc,ifc=xthen0elseπ\\pic\*∑\\sumz,Pxz\*gzc\)

=\(∑\\sumz,Pxz\*\(∑\\sumc,π\\pic\*gzc\)\)\-π\\pix\*\(∑\\sumz,Pxz\*gzx\):=by

havedrop:\(∑\\sumc,ifc=xthen0elseπ\\pic\*∑\\sumz,Pxz\*gzc\)

=\(∑\\sumc,π\\pic\*∑\\sumz,Pxz\*gzc\)\-π\\pix\*∑\\sumz,Pxz\*gzx:=by

have:\(∑\\sumc,ifc=xthen0elseπ\\pic\*∑\\sumz,Pxz\*gzc\)

=∑\\sumc,\(\(π\\pic\*∑\\sumz,Pxz\*gzc\)

\-\(ifc=xthenπ\\pix\*∑\\sumz,Pxz\*gzxelse0\)\):=by

applyFinset\.sum\_congrrfl;introc\_;by\_casesh:c=x<;\>simp\[h\]

rw\[this,Finset\.sum\_sub\_distrib,Finset\.sum\_ite\_eq’Finset\.univx\];simp

rw\[drop\]

congr1

havel1:\(∑\\sumc,π\\pic\*∑\\sumz,Pxz\*gzc\)=∑\\sumc,∑\\sumz,π\\pic\*\(Pxz\*gzc\):=by

applyFinset\.sum\_congrrfl;introc\_;rw\[Finset\.mul\_sum\]

havel2:\(∑\\sumz,Pxz\*\(∑\\sumc,π\\pic\*gzc\)\)=∑\\sumz,∑\\sumc,Pxz\*\(π\\pic\*gzc\):=by

applyFinset\.sum\_congrrfl;introz\_;rw\[Finset\.mul\_sum\]

rw\[l1,l2,Finset\.sum\_comm\]

applyFinset\.sum\_congrrfl;introz\_;applyFinset\.sum\_congrrfl;introc\_;ring

rw\[e1,e2,sa,sb,hret\]

ring

theoremK\_const\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(hirr:∀\\forallxy,∃\\existsn:ℕ\\mathbb\{N\},0<\(P^n\)xy\)

\(K:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hharm:∀\\forallx,Kx=∑\\sumz,Pxz\*Kz\)\(ab:Ω\\Omega\):Ka=Kb:=by

obtain⟨\\langlex0,\-,hx0⟩\\rangle:=Finset\.exists\_max\_imageFinset\.univK

⟨\\langleClassical\.arbitraryΩ\\Omega,Finset\.mem\_univ\_⟩\\rangle

setm:=Kx0withhm

havehmax:∀\\forallz,Kz≤\\leqm:=funz=\>hx0z\(Finset\.mem\_univz\)

havehAclosed:∀\\forallx,Kx=m→\\rightarrow∀\\forallz,0<Pxz→\\rightarrowKz=m:=by

introxhxzhz

exactprop\_stepPhP1hP2Kmhmaxxhx\(hharmx\)zhz

havehall:∀\\forally,Ky=m:=by

introy

obtain⟨\\langlen,hn⟩\\rangle:=hirrx0y

exactreach\_closedPhP1\(funw=\>Kw=m\)hAclosedx0rflnyhn

rw\[halla,hallb\]

theoremtri\_ineq\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(hirr:∀\\forallxy,∃\\existsn:ℕ\\mathbb\{N\},0<\(P^n\)xy\)

\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hg:∀\\forallxy,gxy=ifx=ythen0else1\+∑\\sumz,Pxz\*gzy\)

\(gnn:∀\\forallxy,0≤\\leqgxy\)\(abc:Ω\\Omega\):gab≤\\leqgac\+gcb:=by

by\_caseshbc:b=c

⋅\\cdotsubsthbc

haveh0:gbb=0:=byrw\[hgbb,if\_posrfl\]

have:=gnnab;nlinarith\[h0\]

setθ\\theta:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}:=funx=\>gxb\-gxcwithhθ\\theta

havehharm:∀\\forallx,x≠\\neqb→\\rightarrowx≠\\neqc→\\rightarrowθ\\thetax=∑\\sumz,Pxz\*θ\\thetaz:=by

introxhxbhxc

havegb:gxb=1\+∑\\sumz,Pxz\*gzb:=byrw\[hgxb,if\_neghxb\]

havegc:gxc=1\+∑\\sumz,Pxz\*gzc:=byrw\[hgxc,if\_neghxc\]

simponly\[hθ\\theta\];rw\[gb,gc\]

have:\(∑\\sumz,Pxz\*\(gzb\-gzc\)\)=\(∑\\sumz,Pxz\*gzb\)\-∑\\sumz,Pxz\*gzc:=by

rw\[←\\leftarrowFinset\.sum\_sub\_distrib\];applyFinset\.sum\_congrrfl;introz\_;ring

rw\[this\];ring

obtain⟨\\langlex0,\-,hx0⟩\\rangle:=Finset\.exists\_max\_imageFinset\.univθ\\theta

⟨\\langleClassical\.arbitraryΩ\\Omega,Finset\.mem\_univ\_⟩\\rangle

setm:=θ\\thetax0withhm

havehmax:∀\\forallz,θ\\thetaz≤\\leqm:=funz=\>hx0z\(Finset\.mem\_univz\)

havehθ\\thetac:θ\\thetac=gcb:=bysimponly\[hθ\\theta\];rw\[hgcc,if\_posrfl\];ring

havehθ\\thetab:θ\\thetab=\-gbc:=bysimponly\[hθ\\theta\];rw\[hgbb,if\_posrfl\];ring

havehmeq:m=θ\\thetac:=by

by\_caseshcA:θ\\thetac=m

⋅\\cdotexacthcA\.symm

⋅\\cdotby\_caseshbA:θ\\thetab=m

⋅\\cdotexfalso

haveh1:m≤\\leq0:=byrw\[←\\leftarrowhbA,hθ\\thetab\];linarith\[gnnbc\]

haveh2:0≤\\leqθ\\thetac:=byrw\[hθ\\thetac\];exactgnncb

haveh3:θ\\thetac≤\\leqm:=hmaxc

applyhcA;linarith

⋅\\cdotexfalso

havehAclosed:∀\\forallx,θ\\thetax=m→\\rightarrow∀\\forallz,0<Pxz→\\rightarrowθ\\thetaz=m:=by

introxhxzhz

havehxb:x≠\\neqb:=funh=\>hbA\(h▶\\blacktrianglerighthx\)

havehxc:x≠\\neqc:=funh=\>hcA\(h▶\\blacktrianglerighthx\)

exactprop\_stepPhP1hP2θ\\thetamhmaxxhx\(hharmxhxbhxc\)zhz

obtain⟨\\langlen,hn⟩\\rangle:=hirrx0c

exacthcA\(reach\_closedPhP1\(funw=\>θ\\thetaw=m\)hAclosedx0rflnchn\)

havehθ\\thetaa:θ\\thetaa≤\\leqθ\\thetac:=byrw\[←\\leftarrowhmeq\];exacthmaxa

rw\[hθ\\thetac\]athθ\\thetaa

simponly\[hθ\\theta\]athθ\\thetaa

linarith

theoremcore\_bound\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP1:∀\\forallxy,0≤\\leqPxy\)\(hP2:∀\\forallx,∑\\sumy,Pxy=1\)

\(hirr:∀\\forallxy,∃\\existsn:ℕ\\mathbb\{N\},0<\(P^n\)xy\)

\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hg:∀\\forallxy,gxy=ifx=ythen0else1\+∑\\sumz,Pxz\*gzy\)

\(π\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hpi1:∀\\forallx,0≤\\leqπ\\pix\)\(hpi2:∑\\sumx,π\\pix=1\)

\(hpi3:∀\\forally,∑\\sumx,π\\pix\*Pxy=π\\piy\)

\(M:ℝ\\mathbb\{R\}\)\(hM:∀\\forally:Ω\\Omega,\(∑\\sumx,π\\pix\*gxy\)≤\\leqM\)\(ab:Ω\\Omega\):

gab≤\\leq2\*M:=by

havegnn:∀\\forallxy,0≤\\leqgxy:=funxy=\>g\_nonnegPhP1hP2ghgyx

havehRT:∀\\forallw,π\\piw\*\(1\+∑\\sumz,Pwz\*gzw\)=1:=

funw=\>returnTime\_identityPghgπ\\pihpi2hpi3w

havetri:∀\\forallxyz,gxy≤\\leqgxz\+gzy:=

funxyz=\>tri\_ineqPhP1hP2hirrghggnnxyz

haveKconst:∀\\forallxy,\(∑\\sumc,π\\pic\*gxc\)=\(∑\\sumc,π\\pic\*gyc\):=by

introxy

exactK\_constPhP1hP2hirr\(funx=\>∑\\sumc,π\\pic\*gxc\)

\(funx=\>K\_harmonicPhP1hP2ghgπ\\pihpi1hpi2hRTx\)xy

havehgab:gab≤\\leq\(∑\\sumc,π\\pic\*gac\)\+\(∑\\sumc,π\\pic\*gcb\):=by

haveh1:gab=∑\\sumc,π\\pic\*gab:=byrw\[←\\leftarrowFinset\.sum\_mul,hpi2,one\_mul\]

rw\[h1,←\\leftarrowFinset\.sum\_add\_distrib\]

applyFinset\.sum\_le\_sum;introc\_

havehtri:=triabc

have:π\\pic\*gab≤\\leqπ\\pic\*\(gac\+gcb\):=mul\_le\_mul\_of\_nonneg\_lefthtri\(hpi1c\)

nlinarith\[this\]

havehZb:\(∑\\sumc,π\\pic\*gcb\)≤\\leqM:=hMb

havehKa:\(∑\\sumc,π\\pic\*gac\)≤\\leqM:=by

havehka\_eq:\(∑\\sumc,π\\pic\*gac\)=∑\\sumx,π\\pix\*\(∑\\sumc,π\\pic\*gxc\):=by

have:\(∑\\sumx,π\\pix\*\(∑\\sumc,π\\pic\*gxc\)\)=∑\\sumx,π\\pix\*\(∑\\sumc,π\\pic\*gac\):=by

applyFinset\.sum\_congrrfl;introx\_;rw\[Kconstxa\]

rw\[this,←\\leftarrowFinset\.sum\_mul,hpi2,one\_mul\]

rw\[hka\_eq\]

haveswap:\(∑\\sumx,π\\pix\*\(∑\\sumc,π\\pic\*gxc\)\)=∑\\sumc,π\\pic\*\(∑\\sumx,π\\pix\*gxc\):=by

havel1:\(∑\\sumx,π\\pix\*\(∑\\sumc,π\\pic\*gxc\)\)=∑\\sumx,∑\\sumc,π\\pix\*\(π\\pic\*gxc\):=by

applyFinset\.sum\_congrrfl;introx\_;rw\[Finset\.mul\_sum\]

havel2:\(∑\\sumc,π\\pic\*\(∑\\sumx,π\\pix\*gxc\)\)=∑\\sumc,∑\\sumx,π\\pic\*\(π\\pix\*gxc\):=by

applyFinset\.sum\_congrrfl;introc\_;rw\[Finset\.mul\_sum\]

rw\[l1,l2,Finset\.sum\_comm\]

applyFinset\.sum\_congrrfl;introc\_;applyFinset\.sum\_congrrfl;introx\_;ring

rw\[swap\]

calc\(∑\\sumc,π\\pic\*\(∑\\sumx,π\\pix\*gxc\)\)≤\\leq∑\\sumc,π\\pic\*M:=by

applyFinset\.sum\_le\_sum;introc\_

exactmul\_le\_mul\_of\_nonneg\_left\(hMc\)\(hpi1c\)

\_=M:=byrw\[←\\leftarrowFinset\.sum\_mul,hpi2,one\_mul\]

linarith

endQ361Helpers

openAutoin

theoremq361\_hitting\_bound\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[NonemptyΩ\\Omega\]\[DecidableEqΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP:IsStochasticP\)\(hirr:IsIrreducibleP\)

\(g:Ω\\Omega→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hg:IsHittingSolutionPg\)

\(π\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(hπ\\pi:IsStationaryPπ\\pi\):

\(⨆\\bigsqcupp:Ω\\Omega×\\timesΩ\\Omega,gp\.1p\.2\)≤\\leq2\*⨆\\bigsqcupw,∑\\sumx,π\\pix\*gxw:=by

obtain⟨\\langlehP1,hP2⟩\\rangle:=hP

obtain⟨\\langlehpi1,hpi2,hpi3⟩\\rangle:=hπ\\pi

havehreach:∀\\forallxy,∃\\existsn:ℕ\\mathbb\{N\},0<\(P^n\)xy:=by

introxy

obtain⟨\\langlen,\_,hn⟩\\rangle:=hirrxy

exact⟨\\langlen,hn⟩\\rangle

setM:=⨆\\bigsqcupw,∑\\sumx,π\\pix\*gxwwithhMdef

havehbddM:BddAbove\(Set\.range\(funw=\>∑\\sumx,π\\pix\*gxw\)\):=Finite\.bddAbove\_range\_

havehZle:∀\\forally:Ω\\Omega,\(∑\\sumx,π\\pix\*gxy\)≤\\leqM:=funy=\>le\_ciSuphbddMy

applyciSup\_le

introp

exactQ361Helpers\.core\_boundPhP1hP2hreachghgπ\\pihpi1hpi2hpi3MhZlep\.1p\.2

![Refer to caption](https://arxiv.org/html/2609.09264v1/a1.png)Figure 2:Main logical dependencies in the generated proof of Q361\. Shared maximum\-principle lemmas establish Kemeny constancy and the hitting\-time triangle inequality, which are combined by stationary averaging to prove the bound\. Nodes give Lean theorem names and their mathematical roles; dashed arrows indicate results supplied as hypotheses to later lemmas\.

### A\.2A direct proof example \- Opus Prover

We illustrate Q222 through its natural\-language statement, Lean abstraction, and an agent\-generated proof obtained in a separate run lasting less than 15 minutes\.

#### Natural\-language statement\.

Suppose that P is irreducible\. Show that there exists a probability measureπ\\pisuch thatπ=π​P\\pi=\\pi Pandπ⁡\(x\)\>0\\pi\(x\)\>0for allx∈Ωx\\in\\Omega\.

#### Formalization\.

The Lean statement represents the chain by a real transition matrixPPon a finite, nonempty state spaceΩ\\Omega\. The assumptionsIsStochasticandIsIrreduciblespecify nonnegative entries, unit row sums, and reachability through positive entries of matrix powers\. A stationary probability measure is represented by a functionπ:Ω→ℝ\\pi:\\Omega\\to\\mathbb\{R\}satisfying

π⁡\(x\)≥0,∑x∈Ωπ⁡\(x\)=1,∑x∈Ωπ⁡\(x\)​P​\(x,y\)=π⁡\(y\)\.\\pi\(x\)\\geq 0,\\qquad\\sum\_\{x\\in\\Omega\}\\pi\(x\)=1,\\qquad\\sum\_\{x\\in\\Omega\}\\pi\(x\)P\(x,y\)=\\pi\(y\)\.
importMathlib

importLeanproj\.Basic

openMeasureTheoryProbabilityTheoryFilter

openscopedENNRealNNRealTopologyMatrix

openAuto

variable\{Ω\\Omega:Type\*\}\{m0:MeasurableSpaceΩ\\Omega\}

privatedefstepMap\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(v:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\):Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}:=

funy=\>∑\\sumx,vx\*Pxy

privatenoncomputabledefcesaro\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(v0:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\)

\(N:ℕ\\mathbb\{N\}\):Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}:=

funy=\>\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)y

privatelemmastepMap\_mem\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\{P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\}

\(hP0:∀\\forallxy,0≤\\leqPxy\)\(hP1:∀\\forallx,∑\\sumy,Pxy=1\)

\{v:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\}\(hv:v∈\\instdSimplexℝ\\mathbb\{R\}Ω\\Omega\):stepMapPv∈\\instdSimplexℝ\\mathbb\{R\}Ω\\Omega:=by

refine⟨\\langlefuny=\>?\_,?\_⟩\\rangle

⋅\\cdotshow0≤\\leq∑\\sumx,vx\*Pxy

exactFinset\.sum\_nonneg\(funx\_=\>mul\_nonneg\(hv\.1x\)\(hP0xy\)\)

⋅\\cdotshow∑\\sumy,∑\\sumx,vx\*Pxy=1

rw\[Finset\.sum\_comm\]

calc∑\\sumx,∑\\sumy,vx\*Pxy=∑\\sumx,vx\*∑\\sumy,Pxy:=by

applyFinset\.sum\_congrrfl;introx\_;rw\[Finset\.mul\_sum\]

\_=∑\\sumx,vx\*1:=byapplyFinset\.sum\_congrrfl;introx\_;rw\[hP1x\]

\_=∑\\sumx,vx:=byapplyFinset\.sum\_congrrfl;introx\_;rw\[mul\_one\]

\_=1:=hv\.2

privatelemmapow\_nonneg\_entries\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[DecidableEqΩ\\Omega\]\{P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\}

\(hP0:∀\\forallxy,0≤\\leqPxy\):∀\\forallnxy,0≤\\leq\(P^n\)xy:=by

intron

inductionnwith

\|zero=\>introxy;rw\[pow\_zero\];by\_casesh:x=y<;\>simp\[Matrix\.one\_apply,h\]

\|succnih=\>

introxy

rw\[pow\_succ,Matrix\.mul\_apply\]

exactFinset\.sum\_nonneg\(funz\_=\>mul\_nonneg\(ihxz\)\(hP0zy\)\)

privatelemmastationary\_pow\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[DecidableEqΩ\\Omega\]\{P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\}

\{π\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\}\}\(hstat:∀\\forally,∑\\sumx,π\\pix\*Pxy=π\\piy\):

∀\\forallny,∑\\sumx,π\\pix\*\(P^n\)xy=π\\piy:=by

intron

inductionnwith

\|zero=\>

introy

rw\[pow\_zero\]

simp\[Matrix\.one\_apply,Finset\.sum\_ite\_eq’\]

\|succnih=\>

introy

calc∑\\sumx,π\\pix\*\(P^\(n\+1\)\)xy

=∑\\sumx,∑\\sumz,π\\pix\*\(\(P^n\)xz\*Pzy\):=by

applyFinset\.sum\_congrrfl;introx\_

rw\[pow\_succ,Matrix\.mul\_apply,Finset\.mul\_sum\]

\_=∑\\sumz,∑\\sumx,π\\pix\*\(\(P^n\)xz\*Pzy\):=Finset\.sum\_comm

\_=∑\\sumz,\(∑\\sumx,π\\pix\*\(P^n\)xz\)\*Pzy:=by

applyFinset\.sum\_congrrfl;introz\_

rw\[Finset\.sum\_mul\];applyFinset\.sum\_congrrfl;introx\_;ring

\_=∑\\sumz,π\\piz\*Pzy:=by

applyFinset\.sum\_congrrfl;introz\_;rw\[ihz\]

\_=π\\piy:=hstaty

theoremq222\_stationary\_existence\_positive\{Ω\\Omega:Type\*\}\[FintypeΩ\\Omega\]\[DecidableEqΩ\\Omega\]\[NonemptyΩ\\Omega\]

\(P:MatrixΩ\\OmegaΩ\\Omegaℝ\\mathbb\{R\}\)\(hP:IsStochasticP\)\(hirr:IsIrreducibleP\):

∃\\existsπ\\pi:Ω\\Omega→\\rightarrowℝ\\mathbb\{R\},IsStationaryPπ\\pi∧\\wedge∀\\forallx,0<π\\pix:=by

obtain⟨\\langlehP0,hP1⟩\\rangle:=hP

obtain⟨\\langlev0,hv0⟩\\rangle:\(stdSimplexℝ\\mathbb\{R\}Ω\\Omega\)\.Nonempty:=Set\.nonempty\_coe\_sort\.mpinferInstance

havehiter:∀\\foralln,\(stepMapP\)^\[n\]v0∈\\instdSimplexℝ\\mathbb\{R\}Ω\\Omega:=by

intron

inductionnwith

\|zero=\>simpaonly\[Function\.iterate\_zero\_apply\]usinghv0

\|succnih=\>rw\[Function\.iterate\_succ\_apply’\];exactstepMap\_memhP0hP1ih

havehbmem:∀\\forallN,cesaroPv0N∈\\instdSimplexℝ\\mathbb\{R\}Ω\\Omega:=by

introN

refine⟨\\langlefuny=\>?\_,?\_⟩\\rangle

⋅\\cdotshow0≤\\leq\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)y

exactmul\_nonneg\(bypositivity\)\(Finset\.sum\_nonneg\(funn\_=\>\(hitern\)\.1y\)\)

⋅\\cdotshow∑\\sumy,\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)y=1

rw\[←\\leftarrowFinset\.mul\_sum,Finset\.sum\_comm\]

rw\[Finset\.sum\_congrrfl\(funn\(\_:n∈\\inFinset\.range\(N\+1\)\)=\>\(hitern\)\.2\)\]

rw\[Finset\.sum\_const,Finset\.card\_range\]

simponly\[nsmul\_eq\_mul,mul\_one,Nat\.cast\_add,Nat\.cast\_one\]

exactone\_div\_mul\_cancel\(bypositivity\)

havehdiff:∀\\forallNy,stepMapP\(cesaroPv0N\)y\-cesaroPv0Ny

=\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*\(\(\(stepMapP\)^\[N\+1\]v0\)y\-v0y\):=by

introNy

havehTb:stepMapP\(cesaroPv0N\)y

=\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\+1\]v0\)y:=by

show∑\\sumx,cesaroPv0Nx\*Pxy=\_

havee1:∀\\forallx,cesaroPv0Nx\*Pxy

=\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)x\*Pxy:=by

introx

show\(\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)x\)\*Pxy=\_

rw\[mul\_assoc,Finset\.sum\_mul\]

rw\[Finset\.sum\_congrrfl\(funx\(\_:x∈\\inFinset\.univ\)=\>e1x\),←\\leftarrowFinset\.mul\_sum\]

congr1

rw\[Finset\.sum\_comm\]

applyFinset\.sum\_congrrfl;intron\_

show∑\\sumx,\(\(stepMapP\)^\[n\]v0\)x\*Pxy=\(\(stepMapP\)^\[n\+1\]v0\)y

rw\[Function\.iterate\_succ\_apply’\];rfl

havehbNy:cesaroPv0Ny

=\(1/\(N\+1:ℝ\\mathbb\{R\}\)\)\*∑\\sumn∈\\inFinset\.range\(N\+1\),\(\(stepMapP\)^\[n\]v0\)y:=rfl

rw\[hTb,hbNy,←\\leftarrowmul\_sub\]

congr1

rw\[←\\leftarrowFinset\.sum\_sub\_distrib,Finset\.sum\_range\_sub\(funn=\>\(\(stepMapP\)^\[n\]v0\)y\)\]

simp\[Function\.iterate\_zero\_apply\]

havehtend0:∀\\forally,Filter\.Tendsto\(funN=\>stepMapP\(cesaroPv0N\)y\-cesaroPv0Ny\)

Filter\.atTop\(nhds0\):=by

introy

refinesqueeze\_zero\_norm\(funN=\>?\_\)tendsto\_one\_div\_add\_atTop\_nhds\_zero\_nat

rw\[hdiffNy,norm\_mul\]

haveha:=mem\_Icc\_of\_mem\_stdSimplex\(hiter\(N\+1\)\)y

havehb:=mem\_Icc\_of\_mem\_stdSimplexhv0y

rw\[Set\.mem\_Icc\]athahb

havehcnn:\(0:ℝ\\mathbb\{R\}\)≤\\leq1/\(\(N:ℝ\\mathbb\{R\}\)\+1\):=bypositivity

rw\[Real\.norm\_of\_nonneghcnn\]

havehbound:∥\\\|\(\(stepMapP\)^\[N\+1\]v0\)y\-v0y∥\\\|≤\\leq1:=by

rw\[Real\.norm\_eq\_abs,abs\_le\]

refine⟨\\langle?\_,?\_⟩\\rangle<;\>linarith\[ha\.1,ha\.2,hb\.1,hb\.2\]

calc1/\(\(N:ℝ\\mathbb\{R\}\)\+1\)\*∥\\\|\(\(stepMapP\)^\[N\+1\]v0\)y\-v0y∥\\\|

≤\\leq1/\(\(N:ℝ\\mathbb\{R\}\)\+1\)\*1:=mul\_le\_mul\_of\_nonneg\_lefthboundhcnn

\_=1/\(\(N:ℝ\\mathbb\{R\}\)\+1\):=mul\_one\_

obtain⟨\\langleπ\\pi,hπ\\pisimplex,φ\\varphi,hφ\\varphimono,hφ\\varphitend⟩\\rangle:=\(isCompact\_stdSimplexℝ\\mathbb\{R\}Ω\\Omega\)\.tendsto\_subseqhbmem

havehπ\\picoord:∀\\forallx,Filter\.Tendsto\(funN=\>cesaroPv0\(φ\\varphiN\)x\)Filter\.atTop\(nhds\(π\\pix\)\):=

funx=\>tendsto\_pi\_nhds\.mphφ\\varphitendx

havekey:∀\\forally,∑\\sumx,π\\pix\*Pxy=π\\piy:=by

introy

havehL1:Filter\.Tendsto\(funN=\>∑\\sumx,cesaroPv0\(φ\\varphiN\)x\*Pxy\)Filter\.atTop

\(nhds\(∑\\sumx,π\\pix\*Pxy\)\):=

tendsto\_finset\_sum\_\(funx\_=\>\(hπ\\picoordx\)\.mul\_const\(Pxy\)\)

havehL2:Filter\.Tendsto\(funN=\>cesaroPv0\(φ\\varphiN\)y\)Filter\.atTop\(nhds\(π\\piy\)\):=hπ\\picoordy

havehLdiff:Filter\.Tendsto

\(funN=\>\(∑\\sumx,cesaroPv0\(φ\\varphiN\)x\*Pxy\)\-cesaroPv0\(φ\\varphiN\)y\)

Filter\.atTop\(nhds\(\(∑\\sumx,π\\pix\*Pxy\)\-π\\piy\)\):=hL1\.subhL2

havehL0:Filter\.Tendsto

\(funN=\>\(∑\\sumx,cesaroPv0\(φ\\varphiN\)x\*Pxy\)\-cesaroPv0\(φ\\varphiN\)y\)

Filter\.atTop\(nhds0\):=\(htend0y\)\.comphφ\\varphimono\.tendsto\_atTop

havehuniq:=tendsto\_nhds\_uniquehLdiffhL0

linarith\[huniq\]

refine⟨\\langleπ\\pi,⟨\\langlehπ\\pisimplex\.1,hπ\\pisimplex\.2,key⟩\\rangle,?\_⟩\\rangle

introx0

obtain⟨\\langlea,ha⟩\\rangle:∃\\existsa,0<π\\pia:=by

by\_contrah

push\_negath

haveh0:∑\\sumx,π\\pix=0:=

Finset\.sum\_eq\_zero\(funa\_=\>le\_antisymm\(ha\)\(hπ\\pisimplex\.1a\)\)

rw\[hπ\\pisimplex\.2\]ath0

exactone\_ne\_zeroh0

obtain⟨\\langlen,\_,hn2⟩\\rangle:=hirrax0

havehpow:=stationary\_powkeynx0

rw\[←\\leftarrowhpow\]

refineFinset\.sum\_pos’

\(funx\_=\>mul\_nonneg\(hπ\\pisimplex\.1x\)\(pow\_nonneg\_entrieshP0nxx0\)\)?\_

exact⟨\\langlea,Finset\.mem\_univa,mul\_poshahn2⟩\\rangle

![Refer to caption](https://arxiv.org/html/2609.09264v1/a2.png)Figure 3:Main logical dependencies in the generated proof of Q222\. A telescoping identity and compactness establish a stationary subsequential limit of the Cesàro averages\. Irreducibility and stationarity under matrix powers then yield strict positivity\. Nodes include helper lemmas and local proof facts; edge labels identify supplied hypotheses or supporting arguments\.

### A\.3An abstracted proof example \- Opus Prover

We illustrate Q128 through its natural\-language statement, Lean abstraction, and an agent\-generated proof obtained in a separate run lasting less than 15 minutes\.

#### Natural\-language statement\.

LetBμ​\(t\)=μ​t\+σ​B​\(t\)B\_\{\\mu\}\(t\)=\\mu t\+\\sigma B\(t\)be a Brownian motion with drift\. Show thatBμ​\(t\)−μ​tB\_\{\\mu\}\(t\)\-\\mu tis a martingale, and that\(Bμ​\(t\)−μ​t\)2−σ2​t\(B\_\{\\mu\}\(t\)\-\\mu t\)^\{2\}\-\\sigma^\{2\}tis a martingale\.

#### Formalization\.

The Lean statement uses a real\-valued processBBon a probability space with measureμ\\muand filtrationℱ\\mathcal\{F\}\. Adaptedness and integrability ofBtB\_\{t\}andBt2B\_\{t\}^\{2\}are explicit assumptions\. For0≤s≤t0\\leq s\\leq t,HasLawspecifiesBt−Bs∼𝒩⁡\(0,t−s\)B\_\{t\}\-B\_\{s\}\\sim\\mathcal\{N\}\(0,t\-s\), andIndepspecifies independence of this increment fromℱs\\mathcal\{F\}\_\{s\}\. Lean usesccfor the drift andμ\\mufor the probability measure\. WritingXt=c​t\+σ​BtX\_\{t\}=ct\+\\sigma B\_\{t\}, the conclusion consists of the almost\-sure conditional\-expectation identities

𝔼μ​\[Xt−c​t∣ℱs\]\\displaystyle\\mathbb\{E\}\_\{\\mu\}\[X\_\{t\}\-ct\\mid\\mathcal\{F\}\_\{s\}\]=Xs−c​s,\\displaystyle=X\_\{s\}\-cs,𝔼μ​\[\(Xt−c​t\)2−σ2​t∣ℱs\]\\displaystyle\\mathbb\{E\}\_\{\\mu\}\[\(X\_\{t\}\-ct\)^\{2\}\-\\sigma^\{2\}t\\mid\\mathcal\{F\}\_\{s\}\]=\(Xs−c​s\)2−σ2​s\.\\displaystyle=\(X\_\{s\}\-cs\)^\{2\}\-\\sigma^\{2\}s\.The increment properties are supplied as hypotheses; the proof derives the two identities from these properties\.

importMathlib

importLeanproj\.Basic

openMeasureTheoryProbabilityTheoryFilter

openscopedENNRealNNRealTopologyMatrix

openAuto

variable\{Ω\\Omega:Type\*\}\{m0:MeasurableSpaceΩ\\Omega\}

theoremq128\_drifted\_brownian\_martingale\(μ\\mu:MeasureΩ\\Omega\)\[IsProbabilityMeasureμ\\mu\]

\(ℱ\\mathcal\{F\}:Filtrationℝ\\mathbb\{R\}m0\)\(B:ℝ\\mathbb\{R\}→\\rightarrowΩ\\Omega→\\rightarrowℝ\\mathbb\{R\}\)\(cσ\\sigma:ℝ\\mathbb\{R\}\)

\(hadap:Adaptedℱ\\mathcal\{F\}B\)

\(hint:∀\\forallt,Integrable\(Bt\)μ\\mu\)

\(hint2:∀\\forallt,Integrable\(funω\\omega=\>\(Btω\\omega\)^2\)μ\\mu\)

\(hB0:∀\\forallmω\\omega∂\\partialμ\\mu,B0ω\\omega=0\)

\(hincr:∀\\forallst:ℝ\\mathbb\{R\},0≤\\leqs→\\rightarrows≤\\leqt→\\rightarrow

HasLaw\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\(gaussianReal0\(t\-s\)\.toNNReal\)μ\\mu\)

\(hpast:∀\\forallst:ℝ\\mathbb\{R\},0≤\\leqs→\\rightarrows≤\\leqt→\\rightarrow

Indep\(MeasurableSpace\.comap\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)inferInstance\)\(ℱ\\mathcal\{F\}s\)μ\\mu\):

\(∀\\forallst:ℝ\\mathbb\{R\},0≤\\leqs→\\rightarrows≤\\leqt→\\rightarrow

μ\\mu\[\(funω\\omega=\>\(c\*t\+σ\\sigma\*Btω\\omega\)\-c\*t\)\|\(ℱ\\mathcal\{F\}s\)\]

=m\[μ\\mu\]\(funω\\omega=\>\(c\*s\+σ\\sigma\*Bsω\\omega\)\-c\*s\)\)∧\\wedge

\(∀\\forallst:ℝ\\mathbb\{R\},0≤\\leqs→\\rightarrows≤\\leqt→\\rightarrow

μ\\mu\[\(funω\\omega=\>\(\(c\*t\+σ\\sigma\*Btω\\omega\)\-c\*t\)^2\-σ\\sigma^2\*t\)\|\(ℱ\\mathcal\{F\}s\)\]

=m\[μ\\mu\]\(funω\\omega=\>\(\(c\*s\+σ\\sigma\*Bsω\\omega\)\-c\*s\)^2\-σ\\sigma^2\*s\)\):=by

havehsq\_int:∀\\forallv:NNReal,∫\\intx,x^2∂\\partial\(gaussianReal\(0:ℝ\\mathbb\{R\}\)v\)=\(v:ℝ\\mathbb\{R\}\):=by

introv

havehv:=variance\_of\_integral\_eq\_zero\(μ\\mu:=gaussianReal\(0:ℝ\\mathbb\{R\}\)v\)\(X:=funx=\>x\)

measurable\_id\.aemeasurable\(bysimpausingintegral\_id\_gaussianReal\(μ\\mu:=\(0:ℝ\\mathbb\{R\}\)\)\(v:=v\)\)

rw\[variance\_fun\_id\_gaussianReal\]athv

simpausinghv\.symm

havemain:∀\\forallst:ℝ\\mathbb\{R\},0≤\\leqs→\\rightarrows≤\\leqt→\\rightarrow

\(μ\\mu\[Bt\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]Bs\)∧\\wedge

\(μ\\mu\[funω\\omega=\>\(Btω\\omega\)^2\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]funω\\omega=\>\(Bsω\\omega\)^2\+\(t\-s\)\):=by

introsthshst

havehst0:\(0:ℝ\\mathbb\{R\}\)≤\\leqt\-s:=bylinarith

havehBt:Measurable\(Bt\):=\(hadapt\)\.mono\(ℱ\\mathcal\{F\}\.let\)le\_rfl

havehBs:Measurable\(Bs\):=\(hadaps\)\.mono\(ℱ\\mathcal\{F\}\.les\)le\_rfl

havehg\_meas:Measurable\(funω\\omega=\>Btω\\omega\-Bsω\\omega\):=hBt\.subhBs

havehg\_int:Integrable\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)μ\\mu:=\(hintt\)\.sub\(hints\)

havehindep:=hpaststhshst

havehle1:MeasurableSpace\.comap\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)inferInstance≤\\leqm0:=

hg\_meas\.comap\_le

havehle2:ℱ\\mathcal\{F\}s≤\\leqm0:=ℱ\\mathcal\{F\}\.les

havehsm:StronglyMeasurable\[MeasurableSpace\.comap\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)inferInstance\]

\(funω\\omega=\>Btω\\omega\-Bsω\\omega\):=\(measurable\_iff\_comap\_le\.2le\_rfl\)\.stronglyMeasurable

havehEg:μ\\mu\[funω\\omega=\>Btω\\omega\-Bsω\\omega\]=0:=by

rw\[\(hincrsthshst\)\.integral\_eq,integral\_id\_gaussianReal\]

havehcz:μ\\mu\[funω\\omega=\>Btω\\omega\-Bsω\\omega\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]fun\_=\>\(0:ℝ\\mathbb\{R\}\):=by

haveh:=condExp\_indep\_eqhle1hle2hsmhindep

rw\[hEg\]ath;exacth

havehmart:μ\\mu\[Bt\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]Bs:=by

havehcond\_Bs:μ\\mu\[Bs\|ℱ\\mathcal\{F\}s\]=Bs:=

condExp\_of\_stronglyMeasurablehle2\(hadaps\)\.stronglyMeasurable\(hints\)

havekey:\(Bt\)=\(Bs\)\+\(funω\\omega=\>Btω\\omega\-Bsω\\omega\):=by

funextω\\omega;showBtω\\omega=Bsω\\omega\+\(Btω\\omega\-Bsω\\omega\);ring

havehadd:μ\\mu\[Bt\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]

\(μ\\mu\[Bs\|ℱ\\mathcal\{F\}s\]\+μ\\mu\[funω\\omega=\>Btω\\omega\-Bsω\\omega\|ℱ\\mathcal\{F\}s\]\):=by

calcμ\\mu\[Bt\|ℱ\\mathcal\{F\}s\]=μ\\mu\[\(Bs\)\+\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\|ℱ\\mathcal\{F\}s\]:=

congrArg\(funh=\>μ\\mu\[h\|ℱ\\mathcal\{F\}s\]\)key

\_=m\[μ\\mu\]\_:=condExp\_add\(hints\)hg\_int\_

filter\_upwards\[hadd,hcz\]withω\\omegah1h3

rw\[h1\];simp\[Pi\.add\_apply,hcond\_Bs,h3\]

refine⟨\\langlehmart,?\_⟩\\rangle

havehmemBt:MemLp\(Bt\)2μ\\mu:=

\(memLp\_two\_iff\_integrable\_sqhBt\.aestronglyMeasurable\)\.2\(hint2t\)

havehmemBs:MemLp\(Bs\)2μ\\mu:=

\(memLp\_two\_iff\_integrable\_sqhBs\.aestronglyMeasurable\)\.2\(hint2s\)

havehmemInc:MemLp\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)2μ\\mu:=hmemBt\.subhmemBs

havehd\_int:Integrable\(funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\)μ\\mu:=hmemInc\.integrable\_sq

havehmem2Bs:MemLp\(funω\\omega=\>2\*Bsω\\omega\)2μ\\mu:=hmemBs\.const\_mul2

havehb\_int:Integrable\(\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\)μ\\mu:=

hmem2Bs\.integrable\_mulhmemInc

haveha\_int:Integrable\(funω\\omega=\>\(Bsω\\omega\)^2\)μ\\mu:=hint2s

haveea:μ\\mu\[funω\\omega=\>\(Bsω\\omega\)^2\|ℱ\\mathcal\{F\}s\]=funω\\omega=\>\(Bsω\\omega\)^2:=

condExp\_of\_stronglyMeasurablehle2\(\(hadaps\)\.pow\_const2\)\.stronglyMeasurableha\_int

haveeb:μ\\mu\[\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]fun\_=\>\(0:ℝ\\mathbb\{R\}\):=by

havehpull:=condExp\_mul\_of\_stronglyMeasurable\_left

\(\(\(hadaps\)\.const\_mul2\)\.stronglyMeasurable\)hb\_inthg\_int

filter\_upwards\[hpull,hcz\]withω\\omegah1h3

rw\[h1\];simp\[Pi\.mul\_apply,h3\]

havehsm\_d:StronglyMeasurable\[MeasurableSpace\.comap\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)inferInstance\]

\(funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\):=

\(\(measurable\_iff\_comap\_le\.2le\_rfl\)\.pow\_const2\)\.stronglyMeasurable

havehEd:μ\\mu\[funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\]=t\-s:=by

havehc:=\(hincrsthshst\)\.integral\_comp\(f:=funx:ℝ\\mathbb\{R\}=\>x^2\)\(byfun\_prop\)

simponly\[Function\.comp\_def\]athc

rw\[hc,hsq\_int,Real\.coe\_toNNReal\_hst0\]

haveed:μ\\mu\[funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\|ℱ\\mathcal\{F\}s\]=m\[μ\\mu\]fun\_=\>\(t\-s\):=by

haveh:=condExp\_indep\_eqhle1hle2hsm\_dhindep

rw\[hEd\]ath;exacth

havekey2:\(funω\\omega=\>\(Btω\\omega\)^2\)=

\(funω\\omega=\>\(Bsω\\omega\)^2\)\+\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)

\+\(funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\):=by

funextω\\omega;simponly\[Pi\.add\_apply,Pi\.mul\_apply\];ring

havehcongr:μ\\mu\[funω\\omega=\>\(Btω\\omega\)^2\|ℱ\\mathcal\{F\}s\]=

μ\\mu\[\(funω\\omega=\>\(Bsω\\omega\)^2\)\+\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)

\+\(funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\)\|ℱ\\mathcal\{F\}s\]:=

congrArg\(funh=\>μ\\mu\[h\|ℱ\\mathcal\{F\}s\]\)key2

havee2:μ\\mu\[\(funω\\omega=\>\(Bsω\\omega\)^2\)\+\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\|ℱ\\mathcal\{F\}s\]

=m\[μ\\mu\]\(μ\\mu\[funω\\omega=\>\(Bsω\\omega\)^2\|ℱ\\mathcal\{F\}s\]

\+μ\\mu\[\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\|ℱ\\mathcal\{F\}s\]\):=

condExp\_addha\_inthb\_int\_

havee1:μ\\mu\[\(funω\\omega=\>\(Bsω\\omega\)^2\)\+\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)

\+\(funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\)\|ℱ\\mathcal\{F\}s\]

=m\[μ\\mu\]\(μ\\mu\[\(funω\\omega=\>\(Bsω\\omega\)^2\)\+\(funω\\omega=\>2\*Bsω\\omega\)\*\(funω\\omega=\>Btω\\omega\-Bsω\\omega\)\|ℱ\\mathcal\{F\}s\]

\+μ\\mu\[funω\\omega=\>\(Btω\\omega\-Bsω\\omega\)^2\|ℱ\\mathcal\{F\}s\]\):=

condExp\_add\(ha\_int\.addhb\_int\)hd\_int\_

rw\[hcongr\]

filter\_upwards\[e1,e2,eb,ed\]withω\\omegah1h2hbhd

rw\[h1\]

simponly\[Pi\.add\_apply\]ath2⊢\\vdash

rw\[h2,ea\]

simponly\[Pi\.add\_apply\]athbhd⊢\\vdash

rw\[hb,hd\]

ring

constructor

⋅\\cdotintrosthshst

haveh368:=\(mainsthshst\)\.1

haveharg:\(funω\\omega=\>\(c\*t\+σ\\sigma\*Btω\\omega\)\-c\*t\)=σ\\sigma∙\\bulletBt:=by

funextω\\omega;simponly\[Pi\.smul\_apply,smul\_eq\_mul\];ring

rw\[harg\]

havehsmul:=condExp\_smul\(μ\\mu:=μ\\mu\)σ\\sigma\(Bt\)\(ℱ\\mathcal\{F\}s:MeasurableSpaceΩ\\Omega\)

filter\_upwards\[hsmul,h368\]withω\\omegah1h2

simponly\[Pi\.smul\_apply,smul\_eq\_mul\]ath1

rw\[h1,h2\];ring

⋅\\cdotintrosthshst

havehquad:=\(mainsthshst\)\.2

haveharg:\(funω\\omega=\>\(\(c\*t\+σ\\sigma\*Btω\\omega\)\-c\*t\)^2\-σ\\sigma^2\*t\)=

\(σ\\sigma^2∙\\bullet\(funω\\omega=\>\(Btω\\omega\)^2\)\)\-\(fun\_=\>σ\\sigma^2\*t\):=by

funextω\\omega;simponly\[Pi\.sub\_apply,Pi\.smul\_apply,smul\_eq\_mul\];ring

rw\[harg\]

havehconst:μ\\mu\[\(fun\_=\>σ\\sigma^2\*t\)\|ℱ\\mathcal\{F\}s\]=fun\_=\>σ\\sigma^2\*t:=

condExp\_const\(ℱ\\mathcal\{F\}\.les\)\_

havehsmul:=condExp\_smul\(μ\\mu:=μ\\mu\)\(σ\\sigma^2\)\(funω\\omega=\>\(Btω\\omega\)^2\)\(ℱ\\mathcal\{F\}s:MeasurableSpaceΩ\\Omega\)

havehBt2:MemLp\(Bt\)2μ\\mu:=

\(memLp\_two\_iff\_integrable\_sq

\(\(\(hadapt\)\.mono\(ℱ\\mathcal\{F\}\.let\)le\_rfl\)\.aestronglyMeasurable\)\)\.2\(hint2t\)

havehsub:μ\\mu\[\(σ\\sigma^2∙\\bullet\(funω\\omega=\>\(Btω\\omega\)^2\)\)\-\(fun\_=\>σ\\sigma^2\*t\)\|ℱ\\mathcal\{F\}s\]

=m\[μ\\mu\]\(μ\\mu\[σ\\sigma^2∙\\bullet\(funω\\omega=\>\(Btω\\omega\)^2\)\|ℱ\\mathcal\{F\}s\]\-μ\\mu\[\(fun\_=\>σ\\sigma^2\*t\)\|ℱ\\mathcal\{F\}s\]\):=

condExp\_sub\(Integrable\.smul\(σ\\sigma^2\)hBt2\.integrable\_sq\)\(integrable\_const\_\)\_

filter\_upwards\[hsub,hsmul,hquad\]withω\\omegahs1hs2hq

rw\[hs1\]

simponly\[Pi\.sub\_apply,hconst\]

rw\[hs2\]

simponly\[Pi\.smul\_apply,smul\_eq\_mul\]

rw\[hq\]

ring

![Refer to caption](https://arxiv.org/html/2609.09264v1/a3.png)Figure 4:Main logical dependencies in the generated proof of Q128\. Both conclusions use the zero conditional increment mean\. The squared\-process argument additionally requires the conditional second moment and integrability of the cross term\. Deterministic scaling and subtraction complete the proof\. Nodes name local proof facts and the final theorem; edge labels identify additional hypotheses or algebraic steps\.