lean4

Lean4AgenticRL 提出了首个基于 Lean4 形式化框架的多层级过程奖励方法，用于开放式 agentic RL 训练，并训练出 LAR-9B/27B 模型，其中 LAR-27B 在 TerminalBench-2.1 上达到 77.3%，显著超越同规模领先模型。

介绍 IneqAgent，一个将 LLM 推理与符号计算结合的智能体框架，用于 Lean 4 中的不等式形式化证明，采用 lemma 级蒙特卡洛树搜索协调引理构造与符号后端选择，在四个基准上达到 94.09% 的成功率。

QuixiAI 开源了 Sovereign Protocol Language (SPL)，一个基于 Lean 4 的形式化库，为"主权代理协议"(Protocol of Sovereign Agency) 提供规范性语义，核心包括 Duty、Power、Immunity 等原语以及 Law 3 非干扰实验，全部定理经内核验证、无公理依赖。

Materialize describes how it reworked its `persist` metadata store to build a linearizable log using PostgreSQL's READ COMMITTED isolation instead of SERIALIZABLE, tripling write throughput after a metastable latency incident, and validated correctness by modeling PostgreSQL's behavior in Lean 4 to prove linearizability.

A researcher reports spending three months running Claude Code and Codex on Erdős Problem #993 (unimodality of independent-set sequences in trees), only to learn that Tong Zhang and Wei Li posted a full proof last week, along with two Lean 4 formalizations that claim a clean build. The result is not yet peer-reviewed.

A research team audits OpenAI's Lean 4 formal proof of 3D Navier-Stokes blow-up, showing that while mathematically valid, the solution physically breaks down at the atomic scale (fluid vaporizing at 0.7 nm) — a case of specification gaming. They propose adding a physics-boundary layer to neuro-symbolic AI systems and open-source their verification scripts.

This paper proposes a three-role Monte Carlo Tree Search framework for formal theorem proving in Lean 4, using the compiler as a reward oracle to improve sample efficiency and revealing reward hacking issues through kernel-level proof auditing.

This paper introduces a compiler-guided adaptive proof search framework for context-dependent theorem proving in Lean 4, using cross-model synergy to improve proof success rates while reducing computational cost.

MathForm introduces a framework for mathematical autoformalization using knowledge retrieval and verification-guided refinement, yielding the FormalVerse dataset and an 8B model that outperforms specialized baselines.

PULSE is a new executable contract language for spatiotemporal knowledge graph engineering, providing a typed runtime with role-based write effects, safety properties verified in Lean 4, and trace parity across large datasets.

OpenAI used an internal model, Astra, to solve ten mathematical problems that had stalled for over a decade, spending under $2,000 per problem and releasing Lean 4 formalizations and a paper. The results prompt reflections on AI's role in mathematics.

This paper identifies a fundamental issue in top-k explanations for graph neural networks: automorphisms in input graphs cause non-unique explanations, as the model cannot distinguish symmetric elements. The authors provide a criterion to detect such arbitrariness and verify it using automated reasoning in Lean 4, showing the problem is widespread in molecular datasets.

A DSL based on Google Zanzibar's datalog language for Lean4 to represent and evaluate knowledge bases, manageable under git and without heavy external dependencies.

A formally verified 3D mesh intersection implementation in Lean 4 that requires reviewing only 93 lines of specification, trusting the Lean checker rather than 1000+ lines of AI-generated code. It demonstrates a novel approach to reducing human review effort while ensuring correctness.

This paper presents the design and end-to-end formal verification of IEEE-754 binary32 and bfloat16 arithmetic for ARCH HDL, a hardware description language intended for AI model generation. The operators are proven correctly rounded using a hybrid approach combining exhaustive SMT equivalence checking and Lean 4 proofs, with synthesizable SystemVerilog output.

This article presents Demonstrandum, a verification-first multi-agent AI mathematics pipeline that produces mechanically checkable artifacts, including refutations and proofs of conjectures with Lean 4 kernel verification.

OpenProver is an open-source system for LLM-driven automated theorem proving using Lean 4, featuring a Planner-Worker-Verifier architecture and both autonomous and interactive modes. It enables reproducible evaluation and human-AI synergy in mathematical proof search.

A formalization of combinatorial game theory in Lean 4, covering games, nimbers, and surreal numbers, based on Conway's work.

This paper presents an experience report on a verification pipeline that uses AI provers (Aristotle and Aleph) alongside symbolic extraction tools and formal cryptographic libraries to produce machine-checked correctness proofs for Rust cryptographic code in Lean 4, with case studies from the Ethereum Foundation's zkEVM project.

Introducing Leanstral 1.5, a 119B parameter (6B active) open model for formal proof engineering in Lean 4, achieving 100% on miniF2F, state-of-the-art scores on PutnamBench and FATE benchmarks, and discovering previously unknown bugs in open-source repositories.