We give a machine-checked proof, in Lean 4, of the universal property of multi- centered blowups: given a finite family Z of closed subschemes of a scheme X, presented on each chart by ideals, there is a scheme BlZ X over X, terminal among X-schemes on which every member of the family becomes an effective Cartier divisor. To the best of our knowledge this is the first formalisation of blowups, single- or multicentered, in any theorem prover. The proof is organised around the universal property of the multicentered dilatation of a ring. The comparison isomorphisms on overlaps, the cocycle identity, and the independence of the chosen presentation are obtained from the uniqueness part of this universal property. We give the exact theorem statement as formalized, the proof architecture, and the main new mathematical ingredients, together with the corresponding Lean code.
Jan Dreier, Nikolas Mählmann, Michał Pilipczuk, Szymon Toruńczyk
A graph class $\mathcal{C}$ is monadically dependent if one cannot interpret all graphs in vertex-colored graphs from $\mathcal{C}$ using a fixed formula of first-order logic. We prove that every monadically dependent graph class has almost bounded merge-width, thereby confirming a conjecture of the first and the last author [STOC '25]. Our proof is algorithmic and the witnessing decompositions in the form of merge sequences can be computed in nearly-cubic time. This is a step towards the proof of fixed-parameter tractability of model checking first-order logic on monadically dependent graph classes, which is achieved in a companion paper.
``Emergence'' refers to the fact that different mathematical languages and theories seem to be required to describe scientific theories that operate at different spatial and temporal scales. Highly circumscribed, special cases of emergence have been investigated using many different formal tools, including coarse-graining (over space and / or time), renormalization, dimension reduction, broken symmetry, and various formulations of causality. Here we extend the mathematics of model theory to unify and extend these earlier investigations. As a preliminary application of our framework, we investigate canonical examples of emergence, including the emergence of genetics from chemistry, of psychology from neurobiology, and of different forms of collective behavior from the laws governing their constituent parts. By exploiting the power of model theory we also uncover many aspects of emergence that were previously obscured. In particular, we uncover some of the rich hierarchical structure that relates different scientific fields. For example, we show that scientific fields can be related via a collection of multiple partial orders, all defined over the same set. On the other hand, under an alternative relation among scientific fields, one which allows cycles, we show that it is possible that the set of all of scientific fields must collapse into a single scientific field. Going forward, these investigations point to the formal tools that might need to be developed in order to arrive at a deeper understanding of this emergent hierarchy of scientific reality.
A national digital twin was conceived as an ecosystem of twins connected through mappings to a common foundation, but the roadmap that promises to confirm those mappings are valid never says what valid means. We give the test a precise form, coherence and conservativity of the merged ontology, borrowed from logic-based alignment repair, and apply it to the Information Exchange Standard (IES), first pair by pair and then to whole hubs. Crosswalks from IES into thirteen ontologies across seven sector groups, anchored on the building ontologies BOT, Brick, and SAREF4BLDG, pass through separate stages of matching, human review, certification of each SKOS correspondence against the two class hierarchies, and reasoning with HermiT. Pair by pair, the stages catch different failures: certification alone removed all 526 conservativity violations of the raw crosswalks, review alone left 73, and together they made eleven of twelve overlapping pairs coherent and conservative. Pairwise certification does not compose. Merging the three certified building crosswalks into one hub made five Brick classes unsatisfiable, through a homonym between the IES and Brick notions of a floor that only BOT's disjointness axioms expose; rejecting that one row gave a coherent and conservative hub that entails 290 cross-ontology links nobody wrote down. The core hub is inconsistent before any crosswalk is added, because two published standards, the Open Energy Ontology and BFO 2020, contradict each other; with either one left out it is coherent and conservative. A hub, not a pair, is the unit an ecosystem of twins has to certify.
Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier
We present OCaml and Rocq implementations of Kaplan and Tarjan's purely functional, real-time catenable deques. The correctness of our Rocq code is machine-checked.
While teaching untyped $λ$-calculus to undergraduate students, we were wondering why $α$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $α$-equivalence and show that it conforms to the specification provided in the literature. The work presented in this paper is fully formalized in the Rocq Prover.
Classical Timed Games formulations may be unsuitable, or require substantial modeling effort, to capture complex interaction patterns between a controller and its surrounding environment, in which non-determinism must be resolved after the controller has chosen which action to perform. In this paper, we develop the theory of Timed CLTLoc Games (TCGs), a Timed Game variant designed to facilitate the modeling of such patterns. Unlike classical Timed Games formulations, TCGs partition locations rather than transitions, and use Constraint Linear Temporal Logic over clocks (CLTLoc) to specify the controller's objectives. We develop algorithms for solving TCGs and synthesizing winning controller strategies for games whose objectives include formal properties such as reachability and safety. For reachability objectives, our synthesis algorithm yields winning controller strategies that minimize the number of moves required to reach a goal state. Solving reachability TCGs is EXPTIME-complete, matching the complexity of solving reachability Timed Games. All of our algorithms operate backwards and are implemented in our C++ region-based library TARZAN, leveraging OpenMP for efficient parallelization. Experimental results demonstrate the feasibility of TARZAN.
jq is a widely used tool that provides a programming language to manipulate JSON data. However, the jq language is currently only specified by its implementation, making it difficult to reason about its behaviour. To this end, we provide a formal syntax and denotational semantics for a large subset of the jq language. In particular, we give a translation from jq programs to lambda terms. Our most significant contribution is to provide a new way to interpret updates that allows for more performant execution. We implement our semantics in two interpreters and evaluate the performance.
We confirm a conjecture of the first author [SODA'26] on a strong form of pseudo-telepathy for Khot's $d$-to-$1$ games: for every $d\geq 4$, every $ε>0$, and every $k\in\mathbb N$, there is a $d$-to-$1$ label-cover game of classical value less than $ε$ that admits a perfect quantum strategy using finite-dimensional shared entanglement with measurement contexts of radius at least $k$. As a consequence, there exist graphs whose quantum chromatic number $χ_q$ is $3$ and whose classical chromatic number $χ$ is arbitrarily large. This is the first super-exponential $χ_q$ vs. $χ$ gap, and it improves on the exponential lower bounds of Brassard, Cleve, and Tapp [Phys. Rev. Lett. '99], who produced graphs for which $χ\geq 1.1397^{χ_q}$, and Lalonde, who recently achieved $χ\geq 1.1546^{χ_q}$. To prove the conjecture, we proceed as follows. We start with a ``stretched'' version of the Mermin-Peres magic square, obtained by spacing out its equations and linking them with additional long equation wires. This operation increases the radius of the initial measurement contexts of a perfect quantum strategy for the game, while preserving classical unsatisfiability. We then apply parallel repetition to make the classical value small, and we turn the system into a pseudo-telepathic multi-layered Kneser hypergraph via a PCP construction of Dinur, Guruswami, Khot, and Regev [STOC'03]. Finally, we feed the resulting hypergraph into the reduction of Fei, Minzer, and Wang from hypergraph colouring to $4$-to-$1$ games, we establish quantum completeness of this reduction, and we show that it preserves context radius.
Every fixed first-order sentence $\varphi$ determines an enumerative sequence $n\mapsto \mathrm{FOMC}(\varphi,n)$, counting its models on the labeled domain $[n]$. We study the complexity of these sequences when logical specifications may use genuine unary function symbols and hence nested terms such as $x,f(x),f^2(x),\ldots$. We prove that, for every fixed sentence $\varphi\in \mathrm{C}^1_{=}[f]$ with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(\varphi,n)$ is computable in time polynomial in $n$. By contrast, either a second variable or a second unary function yields hardness: there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete, and there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, with the same property. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $\varphi$, we construct an extension $\varphi_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(\varphi_{\mathrm{aut}},n)=n! \cdot \mathrm{UFOMC}(\varphi,n)$, where $\mathrm{UFOMC}(\varphi,n)$ counts the $n$-element models of $\varphi$ up to isomorphism. This gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. If $\varphi$ belongs to $\mathrm{FO}^k_{=}$, respectively $\mathrm{C}^k$, and its relational vocabulary has maximum arity $r$, eliminating the auxiliary function yields a single-query reduction to labeled model counting in $\mathrm{FO}^{\max\{k,r+1\}}_{=}$, respectively $\mathrm{C}^{\max\{k,r+1\}}$.
Transition Algebra can be viewed as an extension of many-sorted first-order logic by borrowing essential features from dynamic logic. This leads us to new, more expressive sentences that include transitions labelled with actions, which are built from terms using union, composition, and iteration operators. We define a suitable notion of Horn clause, develop a system of proof rules for reasoning about clauses, and subsequently show that the proof system is sound and complete. We then introduce a rewriting relation based on Horn clauses, capturing transitions along established paths expressed as actions. This rewriting relation is naturally extended to a narrowing procedure for solving queries, thereby laying foundation for logic programming in Transition Algebra. As usual, soundness for both rewriting and narrowing is straightforward, whereas completeness requires additional conditions. Finally, we provide a prototype tool that demonstrates the practical aspects and shows the effectiveness of the proposed method.
In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains. Using this forcing method, we derive general criteria that are sufficient for a signature square to satisfy Craig interpolation property.
We develop a boundary-centric semantic framework for higher-order quantum computation, building on the Kelly-Laplaza description of compact closure and Abramsky's execution account. In the semantic carrier Perm(C), morphisms are complex-linear combinations of polarized boundary linkings, composed by execution. Finite-family addresses provide coherent control over finite-level quantum registers (qudits) while retaining the multiplicative boundary structure. We identify essential unitarity, a boundary condition extending ordinary unitarity to higher-order interfaces. On positive qudit registers it coincides with ordinary matrix unitarity; at higher order it expresses preservation of information across the full polarized boundary. We define a unit-free coherent quantum core generated bymultiplicative wiring, unitary gates on positive qudit registers, and contextual coherent control, and prove that every one of its morphisms is essentially unitary. The framework realizes an applied coherent quantum switch and the unitary stages of equal-ratio one-slot supermap dilations with explicit memory. Complete proofs appear in the full version of this paper.
Equational reasoning about circuits underpins quantum-circuit optimisation and verification. In the qubit CNOT-dihedral fragment, phase polynomials and layered normal forms support a complete equational theory. We develop the corresponding theory for prime-dimensional qudits, where basis labels, value controls, and phase exponents share prime-field arithmetic. We first describe reversible affine circuits over F_d as transformations x -> Ax + b, with an affine normal form extending Lafont's linear normal form by translations. Adjoining finite-angle diagonal phases by polynomial degree yields linear, quadratic, and cubic calculi. Their binomial-basis identities expose the mixed diagonal gates forced by affine transport. These calculi have unique phase-affine normal forms, and the resulting equational theories are complete: semantic equality coincides with derivable equality.
E-graphs are a powerful algorithmic technique for automated equational reasoning but have resisted a conceptual understanding independent of issues of presentation and implementation. We propose an operational semantics for e-graphs based on the fundamental category-theoretic concepts of diagrams, limits, and initial functors. We illustrate the formalism through numerous example calculations and establish its soundness and completeness. Technical prerequisites are kept to a minimum in the main text; less standard elements of the mathematical theory are developed in two appendices.
A rule written for people fixes its atomic conditions and connectives but leaves open how the connectives are bracketed, and each bracketing is a different logical reading that an autoformalizer must resolve or expose. We study the scope grammar, a deliberately ambiguous context-free grammar whose derivation trees are the readings of a connective skeleton and whose quotient by logical equivalence is what matters downstream. A skeleton with $k$ binary connectives has $C_k$ derivation trees, the $k$-th Catalan number, but far fewer logically distinct readings. For the positive, repetition-free fragment we make the gap exact: through the uniqueness of the read-once normal form we characterize the realizable normal forms by lowest common ancestors and count them with a two-label recurrence over the operator word, verified against exhaustive enumeration up to eleven atoms. The count is invariant under reversal and $\wedge/\vee$ duality; a skeleton is ambiguous if and only if it uses both $\wedge$ and $\vee$, a one-pass test; and the number of classes is at least $2^{\lfloor n/3\rfloor}$. Up to fifteen atoms the alternating pattern is the worst case; its count has a cubic generating function, is the 3-Schröder sequence (OEIS A137842), and grows with base $\varphi^{5/2}\approx3.330$, below the Catalan base 4. We reduce maximality to an inequality on increments, verified to sixteen atoms, and explain why local exchange arguments cannot prove it. We also treat negation, exceptions, and background axioms, where normal-form uniqueness still decides equivalence but counting is open.
We introduce $n$-almost symmetric Datalog and study $n$-almost symmetric linear arc monadic Datalog. We characterize the finite relational structures whose constraint satisfaction problem is solved by this Datalog fragment as those that can be primitive positively constructed from the transitive tournament on $n+2$ vertices. We also give characterizations in terms of a certain homomorphism duality (which we call $n$-fixed unfolded caterpillar duality) and in universal-algebraic terms (the existence of $k$-absorptive operations and of operations forming an elevator chain of length $n+1$). This article generalizes the results from Bodirsky and Starke about symmetric linear arc monadic Datalog.
Amar Shah, Benjamin F. Jones, Can Cebeci, Jason Z. S. Hu, Lee A. Barnett, Rémi Delmas, Marijn Heule, Bryan Parno 等 9 位作者
We present Sundance, an SMT solver for program verification written in about 13,600 lines of Rust. Sundance combines the Cadical SAT solver with congruence closure, linear arithmetic, algebraic datatypes, and pattern-based quantifier instantiation. Sundance produces eDRAT proofs for every unsat answer. On 21,531 queries from Verus, Dafny, and F*, Sundance is comparable to existing solvers, with 26--38 times fewer lines of code than Z3 and cvc5. We further show that its components can be swapped for Z3's arithmetic solver, MiniSat, and the Semper e-graph. We have open sourced Sundance.
Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux
We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a naïve generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{Ω_k(\sqrt{\lg n})}$ clauses. Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $Ω_k(n^{k}/\lg n)$ in the worst case. In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods.
We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.
Liam Davis, Leopold Haller, Alberto Alfarano, Mark Santolucito
We introduce the Lattice Deduction Transformer (LDT), a recurrent transformer that approximates logically sound deduction by projecting its latent state through a lattice between forward passes. We train on-policy in a process that mirrors deduction in a search-based constraint solver and supervise training via a domain-agnostic approximation of the set of solution candidates based on abstract interpretation. An $800$K-parameter LDT outperforms prior small recurrent reasoners on Sudoku-Extreme with under $2\%$ of their estimated training FLOPs, solving $99.999\%$ of the $422{,}786$ test puzzles. The model is nearly always sound, in that it gives a wrong answer for $4$ of $1.27$M puzzle evaluations, and otherwise returns a correct answer or abstains. A $1.8$M-parameter LDT variant reaches $99.8\%$ accuracy on Maze-Hard. Our code is available at github.com/lcrh/lattice-deduction-transformers.
Recent advances in AI-assisted proof automation are extending the use of proof assistants in software verification and mathematics. However, greater proof automation does not remove users' responsibility to assess whether formal statements capture their intended requirements, making education in formal specification and reasoning essential. To lower the installation and learning barriers associated with mature proof assistants, we present ProofStudio, a browser-based environment integrating Isabelle/HOL, Lean, Rocq, HOL4, and HOL Light with corresponding worked examples, preconfigured proof search, and contextual AI assistance. With ProofStudio, users can explore formal specifications and proofs across five systems without local installation, inspecting native prover feedback and experimenting with automation through a common interface.
LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen, James Shiffer, Saadia Gabriel, Pavel Izmailov
AI 速览：LeanPRM 利用 Lean 证明助手自动为自然语言证明生成步骤级标签，训练无需人工标注的步骤验证器。
AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.
Topological Computational Paths: Presentation Invariance and Observable Quotients
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras
AI 速览：研究有限计算路径的连续表示，比较保留完整带符号轨迹的拓扑与仅记录端点、长度和精确路径实现的可观测拓扑，并分析二者在表示不变性下的差异。
A computational path records the steps used to establish an equality. Topologies on computational equality witnesses can depend on the chosen generators and execution schedule, even when their algebraic and homotopical meanings agree. We study continuous presentations of finite computational paths whose declared rewrites are realized by endpoint-fixed homotopies. We compare a topology retaining the full signed trace with an observable topology recording endpoints, length, and exact path realization. Continuous finite-word interpretations that are inverse up to scoped rewriting preserve trace-sensitive quotient arrows and their final composable-pair spaces. Observable quotients behave differently. Over a point with a nonempty primitive alphabet, we classify their topology: it records length parity when all named relations preserve parity, and is otherwise indiscrete. Adjoining a conservative abbreviation can therefore turn a discrete two-element quotient into an indiscrete space, even though ordinary multiplication remains continuous. A circle presentation also gives nonhomeomorphic quotients under binary and equal-slot timing. Geometric completeness alone does not identify the trace-sensitive and observable topologies. Multiplication is continuous on the quotient of composable representatives. We characterize when this topology agrees with the ordinary pullback topology and give an open-projection criterion. Universal presentations recover classical fundamental-groupoid topology. Normal forms, primitive interchange, and a Cayley covering prove completeness for circle, torus, product, and rose presentations. A literal-word correspondence relates the semantics to the reflexivity, symmetry, and transitivity fragment of equality derivations. Selected results are formalized in Lean, with the realization models and proof coverage stated explicitly.
The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do not directly contribute to it. In the meantime, the growth of Mathlib has recently been bottlenecked by the review process, which requires human reviewers to judge whether proposed pull requests (PRs) follow the Mathlib's conventions and are worth integrating as part of a shared mathematical infrastructure. This leads to our central question: can LLMs help review Mathlib PRs? To this end, we introduce MathlibPR, a benchmark built from real Mathlib4 PR histories. We further propose a staged evaluation protocol and use it to evaluate both LLM models (e.g., DeepSeek, Qwen, Goedel, and Kimina) and LLM agents (e.g., Codex and Claude Code). Surprisingly, both LLM models and LLM agents struggle to distinguish merge-ready PRs from build-passing PRs that were revised or never merged. By turning Mathlib PR histories into a supervised signal, MathlibPR provides a step toward reviewer assistants and reward models that could help evaluate PRs and steer LLMs toward producing merge-ready Mathlib contributions.
Phuong Dang Anh, Duc Nguyen Kim Trung, To Van Khanh
The Distributed Flexible Job Shop Scheduling Problem (DFJSP) requires the joint determination of factory assignment, machine selection, and operation sequencing to minimize the makespan. This paper presents an exact SAT-based approach built on an efficient SAT formulation that exploits problem structure through propagation, symmetry breaking, and incremental SAT solving to effectively address these coupled decisions. The proposed method is evaluated on 76 standard benchmark instances from the Fattahi, Brandimarte, and rdata datasets under two- and three-factory configurations. Together with previously established results, the new SAT optimality certificates bring the total number of proven-optimal instances to 72 out of 76, including three newly certified instances; for two of these instances, SAT also improves the previous best-known makespans. Across the benchmark configurations, SAT achieves the best results on four of the five configurations and remains competitive with strong exact approaches such as CP and LBBD1_CPIL, as well as existing metaheuristic methods. These results demonstrate that the proposed SAT framework is an effective exact approach for the DFJSP, combining strong solution quality with rigorous optimality certification and offering a complementary exact method for future DFJSP studies and evaluations on additional benchmark instances.
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^{Ω(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.
Stefano Berardi, Ugo de'Liguoro, Daniel Osorio-Valencia
We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.
Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a constructive dependent type theory, we present a framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations. We first define open, closed, compact and overt subsets for generic spaces in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis and constructive mathematics. From these proofs we can extract programs for testing inclusion, overlapping of sets, et cetera. To enhance the efficiency of the extracted programs, we then focus on Polish spaces, where we give more efficient encodings based on metric properties of the space. As various computational properties depend on the continuity of the encoding functions, we introduce a nondeterministic version of a continuity principle which is natural in our formalization and valid under the standard type-2 realizability interpretation. Using this principle we further derive the computational equivalence between the generic and the metric encodings. Our theory is fully implemented in the Coq proof assistant. From proofs in this Coq formalization, we can extract certified programs for error-free operations on subsets. As an application, we provide a function that constructs fractals in Euclidean space, such as the Sierpinski triangle, from iterated function systems using the limit operation. The resulting programs can be used to draw such fractals up to any desired resolution.
The GKR soundness theorem bounds the acceptance of a false output claim for a fixed circuit and input. It does not say what the outputs of a compiled circuit mean for that input, and that has to be proved for each family of circuits. For a sparse Merkle tree over a compressing hash, heuristically almost every root admits a valid path for almost any leaf, so the needed statement concerns the witness as well as the claim. We prove per-input soundness for membership, non-membership and update claims, for trees of every depth, in the delegation setting of GKR: the verifier reads the circuit input in the clear and leaves the node hashes to the circuit. Assuming correct hash sub-circuits, every accepted input, honestly encoded or not, determines a valid witness, and the chain constraint cannot be dropped. If the witness read from an input fixed before the challenges is not valid, this verifier accepts with probability at most $\bigl(s_{\mathrm{out}}+\sum_i(8s_i+1)\bigr)/|\mathbb{F}|$ for a circuit with $2^{s_{\mathrm{out}}}$ outputs and $2^{s_i}$ wires read at layer $i$. This covers cube gates for the Poseidon2 S-box and, with $|\mathbb{F}| = p^4$, circuits over the 31-bit KoalaBear field with challenges from its quartic extension. The implemented node hash, a truncated permutation, is not collision resistant, so the statement that accepted runs for one key and root assert the same leaf assumes position binding of the tree. All our results are proved in the paper. Isabelle/HOL also checks a layer-chain bound, the exactness of the verifier's checks on encoded witnesses in a constraint-level model with abstract hash sub-circuits and, over one field, their composition for claims with no valid witness. All bounds concern the interactive public-coin protocol.