Papers

We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.

We introduce a novel functional-style concurrent programming language called Categorical Message Passing Language (CaMPL) which is designed using the mathematics of linear actegories. This mathematical underpinning gives CaMPL programs useful properties such as deadlock freedom, and additionally, livelock freedom for programs without general recursive processes. We explore CaMPL's type system through a series of code examples. The current proto-alpha version of the compiler and the abstract machine is implemented in Haskell. A reader is encouraged to experiment with writing CaMPL programs either using the online compiler https://campl-app.vercel.app/ or by installing CaMPL from https://campl-ucalgary.github.io – our website has detailed instructions on how to run CaMPL code.

Extending the recursion principles of a formal system is an enticing but dangerous endeavour with a well-documented history of leading to consistency bugs. Nakano's guarded recursion is an elegant, type-based approach to soundly extend type theory with a powerful recursion principle. This makes guarded recursion useful for many applications, from programming with infinite structures such as streams to reasoning about advanced programming language features using synthetic guarded domain theory. Sadly, guarded recursion is not directly supported by any major interactive theorem prover, which leaves users of guarded recursion with unmechanised pen-and-paper proofs or mechanisations that depend on unmaintained theorem provers. In this paper, we present an implementation of guarded recursion as an embedded language in Lean consisting of a simply-typed lambda calculus for definitions and a higher-order logic for reasoning. Using Lean's excellent support for metaprogramming, our language allows users to write guarded recursive definitions in an intuitive syntax and to prove properties about them using a dedicated proof mode. We give our language a presheaf model, which we use to prove the soundness of our language and to allow users to export guarded recursive definitions and their theorems into standard Lean developments. To demonstrate the usefulness of our language, we present several case studies for programming and reasoning with guarded recursion.

The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.

We formalize Hastad's PARITY lower bound in Lean using the switching lemma. For every fixed d >= 2, formulas and DAG circuits of computation depth at most d computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))) for all sufficiently large n. This matches the classical upper bound up to constants in the exponent and implies that PARITY is not in nonuniform AC0. We also construct a polynomial-size, logarithmic-depth bounded-fan-in formula family for PARITY, providing a witness to NC1 is not a subset of AC0 for the formalized models. The Lean source code is available at https://github.com/formalcs/circuit-complexity and is checked with Lean 4.33.1 and mathlib 4.33.1.

In dynamic epistemic logic, the four notions of success, self-refutation, true lies, and impossible lies have been discussed in the context of public announcements. In this paper, we introduce eventual and strong eventual versions of these notions, as well as their transfinite versions, which allow transfinite iteration of announcements. We also introduce the notions of always informativeness when true or false. For example, a formula is eventually self-refuting if, whenever initially true, it eventually becomes false at some finite stage under iterated announcements, and strong eventual self-refutation further requires the formula to remain false at all sufficiently late stages. There are two main results. The first result gives the relationship among strong eventual notions, eventual notions, and several other conditions including conditions on the limit of the truth values of the announced formula, the uniform bound condition, and the fixed-point views of the Moore sentence and the self-fulfilling sentence. The second result gives the relationship among finite and transfinite versions of the eventual and strong eventual notions and the fixed-point views.

Given a rational matrix $A$, is every sufficiently large power $A^n$ entrywise nonnegative? We prove that this problem is decidable in deterministic polynomial time. This is in contrast with deciding eventual nonnegativity of a single prescribed entry sequence $(A^n)_{ij}$, which amounts to the Ultimate Positivity Problem for linear recurrence sequences, whose decidability is open. The previous decidability procedure (D'Costa, Ouaknine and Worrell, STACS 2024) splits the matrix powers into residue classes modulo a torsion exponent $D$ whose value can be exponential in the input size. We show that it is sufficient to check a single progression $A^{Dk+1}$: the exponents $n$ with $A^n \geq 0$ are closed under addition, and two consecutive exponents of the progression are coprime, so they generate every sufficiently large exponent. Along the progression, eigenvalues are grouped by their common $D$th power, and the required coefficients for each group are computed without forming $A^D$, any $\lambda^D$, or a splitting field: each summand is evaluated in its own root field $\mathbb{Q}(\lambda)$, and Galois equivariance keeps the degree and height of every class sum polynomially bounded, enabling certified zero and sign tests. The same algorithm with one case rejected decides eventual positivity, and a variant decides whether the matrix has any nonnegative power at all.

An automated fact-checking system returns a label: the claim is true, or it is false. In many such systems the verdict remains the primary output. What is generally missing is a record of which document settled the question, of what would have had to be different for the verdict to change, or of whether the same claim, reworded, would have been judged the same way. We call the missing piece a warrant: a separate statement of what was guaranteed and on what grounds. Formal methods produce evidence of this kind, and regulation is beginning to ask for it, since the Digital Services Act and the AI Act both call for auditable evidence about how systems behave. Surveys of automated fact-checking are usually organised by pipeline stage, and treat logic as one technique among many. We organise the field by what is being formalised instead, which gives five levels: the claim, the reasoning, the system doing the checking, the ecosystem the claim spreads through, and the regulatory obligation. Sorting 121 works into those levels, two patterns stand out. Most of the relevant formal machinery already exists, but it was built for other domains and has rarely been applied here, and the gap is widest for verifying the checking system itself. Several stages of the routine professional fact-checkers follow also have no stated correctness criterion, and two of them, writing a claim in checkable form and correcting a verdict already published, are not formally specified in any work we coded. We close with open problems, each with a suggested first step.

For a propositional proof system $\mathcal{P}$ and a polynomial-time function $G: \{0, 1\}^n \to \{0, 1\}^N$ ($N > 10n$), we say that $G$ is a *proof complexity generator* against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the (suitably encoded) statement "$y\not\in\mathrm{Range}(G)$" for every $y \in \{0, 1\}^N$, and $G$ is a *demi-bits generator* against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the statement "$y \not\in\mathrm{Range}(G)$" for a noticeable fraction of $y \in \{0, 1\}^N$. As can be seen from the definitions, proof complexity generators are qualitatively stronger objects than demi-bits generators. Our main result is that, perhaps counter-intuitively, every demi-bits generator "contains" exponentially many proof complexity generators. In fact, a random subset of output bits of a demi-bits generator forms a proof complexity generator with constant probability. This result is an extremely simple corollary of Pajor's Lemma (a strengthening of the well-known Sauer–Shelah Lemma). This result allows us to exhibit the hardness of the Range Avoidance problem ($\text{Avoid}$) in several new, restricted settings of interest. Along the way, we introduce the notion of *zero-error disperser families* that can transform demi-bits generators into proof complexity generators, and show that this family can be computed by projections (i.e., without any circuit complexity overhead). Using a different instantiation of this family, we construct proof complexity generators from *barely non-trivial* demi-bits generators $G: \{0, 1\}^n \to \{0, 1\}^N$, where the number of hard-to-prove statements of the form "$y \not \in \mathrm{Range}(G)$" just slightly exceeds $2^n$ (which is the number of *false* statements of this form).

The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of $\mathrm{ZF}$. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of $\mathrm{ZF}$, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some $V_\rho$ is already a model of $\mathrm{ZF}$; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way $\mathrm{ZF}$ has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.

Resolution over parities, $\mathrm{Res}(\oplus)$, is the characteristic-two version of resolution over linear equations: clauses are disjunctions of affine equations over $\mathbb F_2$. Superpolynomial size lower bounds were previously known only for restricted refutations: tree-like, regular, or of bounded depth. We prove that every DAG-like $\mathrm{Res} (\oplus)$ refutation of the bit pigeonhole principle with $n+1$ pigeons and $n=2^\ell$ holes has more than $\exp(n/(32768\ell^2))=2^{\Omega(n/\log^2 n)}$ clauses, for every $\ell\ge32$, with no restriction on regularity or depth. The proof translates an arbitrary refutation with $S$ clauses into a polynomial calculus refutation of degree $O(\log n)$ over $O(S+n^2)$ groups of extension variables in the style of Buss, Impagliazzo, Krajicek, Pudlak, Razborov, and Sgall. One substitution then removes all extension variables at once and leaves a nonzero low-degree polynomial derived from the pigeonhole axioms alone at degree at most $n/2$; a degree lower bound in the style of Razborov, proved through the homology of chessboard complexes, shows that no such derivation exists. The argument also yields a general sufficient condition for $\mathrm{Res}(\oplus)$ size lower bounds. The main theorem, this condition, and all their dependencies are formalized in Lean 4, and every statement links to its formal proof. The proof was developed with substantial AI assistance within an open research framework described in the final section.

The category Nom of nominal sets was proposed by Pitts and Gabbay as a setting for the semantics of abstract syntax with variable bindings. It is well-known that Nom is a topos, also known as the Schanuel topos, and in particular it follows that Nom is locally closed, i.e., every slice category Nom/X is cartesian-closed. In this paper, we show that Nom has a much stronger property: every monoidal (closed) structure on Nom induces a monoidal (closed) structure on all slice categories Nom/X. One monoidal closed structure of particular interest on Nom is the separated product A * B, whose right adjoint A -* B is called the separated function space. In particular, it follows that Nom is locally separatedly closed.

Let $B$ be the bluebird combinator with reduction rule $Bxyz \to_{w} x\left(yz\right)$, let $M$ be the mockingbird combinator with reduction rule $Mx \to_{w} xx$, and let $I$ be the identity bird combinator with reduction rule $Ix \to_{w} x$. A fixed-point combinator, called a sage bird by Smullyan, is a closed term $Y$ such that, for a fresh variable $x$, $Yx$ is equivalent to $x\left(Yx\right)$ under these reduction rules. For a fixed variable $x$, we construct an invariant $\mathrm{Tr}_{x}\left(u\right)$ of a $BMI$-term $u$ with respect to $\to_{w}$. This invariant traces the occurrences of $x$ in the leftmost-innermost reduction sequence of $u$. We then prove that $\mathrm{Tr}_{x}\left(Yx\right) \neq \mathrm{Tr}_{x}\left(x^{r}\left( Yx \right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\geq 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic. This provides a negative answer to the problem posed by Smullyan in 1985.

Filter bubbles can be understood as configurations characterized by within-group proximity and separation from outsiders. Personalized feeds may form or preserve such configurations. We develop hybrid-style logics for reasoning about filter bubbles. The static logic characterizes bubble-shaped configurations, while its dynamic extension captures their formation and persistence under personalized feeds. We provide sound and strongly complete axiomatizations for the static and dynamic logics and prove their decidability.

Symmetry breaking in graph search problems remains challenging: complete symmetry breaking constraints are typically exponential in size, while partial approaches trade precision for scalability. We introduce a strength-driven, redundancy-aware methodology for constructing compact partial symmetry breaking constraints based on graph patterns. Each pattern corresponds to a Boolean clause over equality literals and can be integrated directly into CP or SAT models. Our approach incrementally selects strong, non-redundant graph patterns, yielding partial symmetry breaks that achieve substantial pruning of non-canonical graphs while remaining compact in size. This provides a principled framework for deriving lightweight partial symmetry breaking constraints which are significantly more precise than all published state-of-the-art alternatives. We evaluate the proposed constraints on graph instances with up to 25 vertices using a redundancy ratio metric. The resulting partial symmetry breaks constitute only a small fraction of the size of complete symmetry breaking constraints, while delivering significant performance improvements across several graph search benchmarks compared to previously defined partial symmetry breaking methods.

Chain-of-Thought (CoT) reasoning has been shown to improve the performance of large language models (LLMs), yet existing optimization methods largely rely on outcome-based feedback, leaving the logical validity of intermediate reasoning steps largely unverified. To address the gap whereby LLMs arrive at correct final answers through logically flawed intermediate reasoning chains, we propose LogicTrack, a neuro-symbolic framework that audits reasoning trajectories by auto-formalizing each reasoning step into symbolic representations and verifying it with automated theorem provers. LogicTrack introduces Solver-Based Backtracking Reward (SBR), a step-wise scoring mechanism that quantifies logical soundness and guides backtracking tree search at inference time. We further extend LogicTrack to construct supervised fine-tuning (SFT) data with backtracking traces from its trajectories, enabling fine-tuned models to internalize step-wise auditing as an intrinsic capability. Extensive experiments across 8 reasoning benchmarks and 7 LLMs demonstrate that LogicTrack effectively improves both the verifiability of reasoning chains and final answer pass rate, thereby enhancing overall CoT quality and trustworthiness in high-stakes domains.

In this paper, we define a formula $\varphi$ to be unbelievable if $\Box\varphi$ is unsatisfiable, and unknowable if $\Box\varphi\land\varphi$ is unsatisfiable. We then analyze the sources of unknowability and unbelievability in different classes of frames K, KD, KD45, and S5. We first show that any unbelievable formula is a fixed point of the Moore function defined by $f(\varphi)=\varphi\land\lnot\Box\varphi.$ Our main result shows that in S5, the static notions of unknowability and unbelievability in epistemic logic, and the dynamic notions of always informativeness and eventual self-refutation in dynamic epistemic logic are all equivalent to “Moorean phenomena.” We also generalize the result to the multi-agent case, showing that although all unknowable formulas still manifest Moorean phenomena, new mechanisms arise due to their interactive nature. Finally, we briefly analyze whether the Brandenburger-Keisler paradox in epistemic game theory can be considered Moorean.

We demonstrate that forking in monadically NIP theories satisfies a very strong form of triviality over arbitrary sets, generalizing Baldwin-Shelah in monadically stable theories and analogous to Shelah's result for finite satisfiability over models in monadically NIP theories. This implies in particular that strict non-forking independence is particularly well behaved, and that the forking relation induces a canonical semilinear partial order on singletons. We also give an example of an $\omega$-categorical monadically NIP theory so that no finite set is an extension base.

Kaplansky's zero-divisor conjecture asserts that the group ring of a torsion-free group over a field has no zero divisors. It holds for every group with the unique-product property, so a counterexample can only come from a torsion-free group without unique products. In lectures in 2021, Gardam announced that the torsion-free $\tilde{A}_2$ lattice $\Gamma = \langle a, b \mid a b a^2 b^{-1} a^2 b^{-2}, a b^3 a b^4 a^{-1} b \rangle$ does not have unique products and presented it as a new candidate group: it has property (T), and the known methods for proving the conjecture do not apply to it. To our knowledge, no proof of the announcement has been published. We give a proof checked by the Lean 4 kernel and stated against Mathlib's UniqueProds class. The witness is an explicit pair of finite subsets with $|A| = 32$ and $|B| = 28$ in which each of the 896 products coincides with another product. For 658 products the certificate is an identity in the free group; the other 238 certificates are explicit products of conjugated relators, 970 conjugates in all, checked by free reduction. A homomorphism onto $\mathbb{Z}/42$ shows that each pair $(u,v)$ differs from its partner $(u',v')$ as a pair of group elements, which is all the theorem requires. Together with a homomorphism onto the alternating group $A_4$ it also shows that the listed words are pairwise distinct, so the sets have exactly 32 and 28 elements. The witness and certificates come from an untrusted search program and are re-checked by Lean. The development uses only the axioms propext, Classical.choice and Quot.sound, with no sorry and no native_decide. The mathematical statement is Gardam's. To our knowledge this is the first verification in a proof assistant of a unique-product failure in a torsion-free group; torsion-freeness of $\Gamma$ is taken from Gardam and is not formalized here.

Robustness analysis plays a central role in the verification and design of computational and hybrid systems, particularly when system behaviour depends continuously on parameters subject to perturbation. Existing domain-theoretic frameworks provide a principled foundation for reasoning about such perturbations via monotone maps on lattices of closed sets. However, these frameworks face significant limitations when the underlying state space is not locally compact, as is the case for the infinite-dimensional spaces that arise in analysis, machine learning, and control theory (e.g., $\ell_p$ and $L_p$ spaces). In these settings, the lattice of closed subsets fails to be continuous, and classical compactifications either sacrifice precision or lack computable structure. We propose Gromov's horofunction compactification as a new tool for robustness analysis over a class of separable metric spaces of practical importance, including separable reflexive Banach spaces. Given a metric space $\mathbb{S}$, we show that its horofunction extension yields a compact metric space together with a Lipschitz embedding, which enables robust approximations of monotone maps via Scott-continuous maps on the compactified domain. For separable spaces, the horofunction compactification is metrizable, which provides a path toward effective domain-theoretic constructions.

The EU AI Act mandates that datasets for high-risk machine learning (ML) systems meet strict quality criteria such as soundness and bias mitigation. While Satisfiability Modulo Theory (SMT) solving offers a formal approach to verifying these properties, its scalability in realistic ML settings remains unexplored. To bridge this gap, this work presents the first large-scale empirical study of SMT-based dataset verification on two real-world ML datasets. We systematically evaluate how solver performance is shaped by three key dimensions: the type of data-quality property, the specification style, and the dataset encoding strategy. Our findings demonstrate that SMT-based verification is feasible for practical scenarios, but each dimension shapes it: the property type sets the tractability limit, the specification style drives scalability (exceeding $2{,}000{\times}$ for aggregate properties), and the encoding strategy has a systematic effect, with extracted feature columns performing best.

Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, large language models (LLMs) have recently emerged as surprisingly effective optimizers when coupled with iterative prompting. In this work, we connect these ideas and introduce LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, our key idea is to expose the LLM to semantic information that is natural for language models but absent from standard numerical optimizers, including natural-language input and output names, output trajectories, and critical-time witnesses for the minimum robustness value. These additions enable smarter and more sample-efficient robustness search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications when measured by the average number of simulations required to find a counterexample.

Run two process-discovery algorithms on the same event log and they return two different pictures of the same process. Petri nets, causal nets, process trees and BPMN each rely on routing machinery of their own, and their only common ground is the traces they generate. A trace lists activities one after another, so it discards the concurrency the notations exist to express, and two models with identical trace languages can describe genuinely different processes. Whether two discovered models mean the same thing therefore has no notation-independent answer. We show that all four notations admit one canonical presentation, a signature recording a model's activities and the typed interfaces along which they compose, and nothing of the routing machinery. Four construction theorems establish this presentation notation by notation, so two models are compared in a form that each notation determines on its own. Signature equality implies trace equivalence and is strictly finer, separating genuine concurrency from interleaved choice, which a trace comparison cannot, and signature inclusion implies trace inclusion. In a recovery study on one object-centric log, the discovered causal net has exactly the ground-truth signature, while the discovered Petri net's signature strictly contains it and locates every behaviour the Petri net adds in its silent structure. The gain is largest for object-centric data, where a single log supports several notations at once. The four notations become one calculus, in which a translation between them is a claim that can be checked.

We develop a new framework for proving the undecidability of first-order theories of structures of the form $\langle \mathbb{N}; +, P \rangle$, $\langle \mathbb{N}; <, f \rangle$, and $\langle \mathbb{N}; +, f\rangle$, where $P \subseteq \mathbb{N}$ and $f \colon \mathbb{N} \to \mathbb{N}$. It is based on the recent proof of Hieronymi and Schulz that the first-order theory of $\langle \mathbb{N}; +, \{2^n \colon n \in \mathbb{N}\}, \{3^n \colon n \in \mathbb{N}\}\rangle$ is undecidable, and capable of transforming various randomness results about integer sequences into undecidability proofs. We apply our method to a large class of integer linear recurrence sequences, as well as various special functions, in particular showing that the first-order theories of $\langle \mathbb{N}; +, \{u_n \colon n \in \mathbb{N}\} \cap \mathbb{N}\rangle$, $\langle\mathbb{N}; <, n \mapsto \max\{0,u_n\}\rangle$, and $\langle \mathbb{N}; <, \phi\rangle$ are undecidable, where $(u_n)_{n\in\mathbb{N}}$ is any integer LRS with exactly two non-repeated dominant roots satisfying a non-degeneracy assumption, and $\phi$ is Euler's totient function.

Escardó's dialogue interpretation assigns to each closed term $t:(\iota\to\iota)\to\iota$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $\iota$ is the natural-number type. We give a direct proof that its classical ordinal height is below $\epsilon_0$. More precisely, we compute a natural number $K(t)\ge2$ from the type levels occurring in the source term and prove $h(D(t))<\theta_{K(t)}$, where $\theta_0=\omega$ and $\theta_{n+1}=\omega^{\theta_n}$. Our proof translates recursors into closed infinitary templates and eliminates $\beta$-redexes by a finite sequence of passes indexed by ordinary type level. The translation and every pass preserve the dialogue denotation exactly. An auxiliary rank $\rho$ satisfies an additive substitution bound; each pass sends rank $\alpha$ to at most $2^\alpha$. Combining these estimates with a computable initial bound $\omega+m(t)$ and a dialogue-height bound $2^{\rho(N)}$ for closed ground normal forms $N$ yields the stated tower bound. A semantics-preserving translation transfers the result to Escardó's original combinatory interpretation. We formalise the proof in Agda over classical ordinals under explicit foundational assumptions.

We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techniques lead to a synthetic Taylor formula for a Riemannian metric in normal coordinates, which is the main contribution of this work.

Characterizing LLM reasoning remains an open challenge, as many existing benchmarks isolate specific reasoning skills, rely on external knowledge, or are costly to extend. We introduce PetriBench, a compact, fully self-contained, and scalable benchmark for evaluating LLM reasoning over dynamic state spaces using Petri nets, a mature formalism for modeling real-world concurrent and distributed systems. PetriBench organizes reasoning into four task families varying by scope and temporal horizon, with Easy, Medium, and Hard levels generated by increasing structural complexity and evaluated against exact ground truth. Across a diverse set of proprietary and open-weight models, accuracy decreases consistently with difficulty, while harder instances expose increasingly distinct task-specific capability profiles. Additional analyses show that test-time compute improves performance but interacts differently with different reasoning tasks, and that procedural generation yields smooth scaling with structural complexity. Together, these results show that PetriBench provides a unified and extensible setting for probing the strengths, limits, and scaling behavior of LLM reasoning.

Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software engineering principles and practices, it uses a shared blueprint to guide nested planning, proving and review loops. Agents strengthen verification and review throughout formalization. We completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.

While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating informal natural language into a formal language is a critical data bottleneck plagued by an "illusion of rigor": standard type-checkers accept statements that compile but drop hypotheses, introduce vacuous truths, or subtly alter mathematical bounds. To resolve this, we introduce Sage (Semantic Agent-Guided Formalization Engine), an agentic framework that replaces monolithic translation with a four-stage decomposed generation pipeline coupled with a dual-signal semantic correction loop. By pairing Lean 4 compiler diagnostics with multi-dimensional semantic feedback, our correction loop enforces mathematical fidelity alongside syntactic validity. By explicitly accounting for the gap between open-ended queries and declarative formal targets, our pipeline prevents models from achieving high formalization rates by guessing unverified answers (exhibiting a 70.9% answer leakage rate in monolithic baselines). Consequently, Sage suppresses leakage to 2.7% while achieving 73.3% pass@4 joint compilation and semantic fidelity on the Omni-MATH without proofs (compared to 42.0% for a fine-tuned Goedel-Formalizer-V2 baseline). Finally, on IMO-Unformalized, a novel frontier of 175 unformalized International Mathematical Olympiad problems, Sage demonstrates effective zero-shot generalization with 87.4% pass@4 verified fidelity compared to just 19.4% for the baseline, winning over 79% of blind pairwise evaluations.

A 2021 proof of a special case of the Union-Closed Conjecture, by Aaronson, Ellis and Leader, has been formalised in the proof assistant Isabelle/HOL. Our discussion involves sketching their proof and displaying snippets from the Isabelle version of the proof, illustrating the extent to which mathematical reasoning can be rendered clearly in a formal language.