Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once through a case split on whether the always-diverging program bot satisfies the property in question. We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP): valid in intuitionistic logic, requiring neither diagonalization nor self-reference, and adding no classical reasoning beyond the MRDP assumption itself. The key idea is a two-witness construction. Given a non-trivial property P, we attach to each Diophantine polynomial D a pair of programs S^0_D, S^1_D that behave like the negative and positive witnesses for P when D is solvable, and both diverge identically when it is not. A hypothetical decider for P would therefore decide Diophantine solvability via the difference delta_D = DecideP(S^1_D) - DecideP(S^0_D) -- contradicting the MRDP theorem. The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot). The undecidability of the halting problem follows as an immediate corollary: a single application of Rice's theorem to the Terminates property. A formalization in the Rocq proof assistant confirms both results within a step-indexed model of computation, with the undecidability of Hilbert's Tenth Problem as the sole external axiom. Both Rice_Theorem and Halting_Problem are closed under the global context.
Michael Benedikt, Chia-Hsuan Lu, Alex Perry, Tony Tan
We look at a two-variable logic over finite graphs that allows Presburger quantifiers: linear arithmetic inequalities between the number of elements that satisfy subformulas. The prior literature shows that closing two-variable logic under Presburger quantification leads to undecidability, while closing under \emph{local quantification} -- the counts are always over neighbors of a given node -- preserves decidability. Here we show decidability of satisfiability for an intermediate logic that allows both local counts and global counts, but where the linear constraints do not mix the two. The proof requires a significant extension of the prior machinery developed for two-variable logic with counting. As a corollary we obtain decidability of satisfiability for an important family of Graph Neural Networks (GNNs). GNNs are a popular graph learning formalism. For example, in a variation of GNNs considered in the past literature, local aggregation is used in each layer to create modified values at each vertex of a graph, and then global aggregation is used in a final layer to obtain a single numerical value for the graph as a whole. Our logic is motivated by the fact that mixing of local counting and global aggregation in GNNs has been shown to lead to undecidability. Our results here show that if global and local aggregation are separated, one regains decidability. Decidability of other static analysis problems, like equivalence of GNNs, follows from the decidability of satisfiability.
A differential category is an additive symmetric monoidal category with an algebra modality, axiomatizing smooth functions, and a deriving transformation, axiomatizing the differentiation of these smooth functions. An algebra modality may or may not have both the nullary and the binary Seely isomorphisms. Lemay proved that if an algebra modality has both Seely isomorphisms, then it has at most one deriving transformation. It was then an open problem whether every algebra modality has at most one deriving transformation. We answer this question in the negative by constructing algebra modalities with infinite sets of deriving transformations. We also clarify the relations between the nullary Seely isomorphism, the binary Seely isomorphism, and uniqueness of deriving transformations (that is, the property for an algebra modality to have at most one deriving transformation). First, we refine Lemay's theorem by removing the assumption of the nullary Seely isomorphism. Then, we show by means of various examples that the six combinations of absence or presence of nullary Seely isomorphism, binary Seely isomorphism, and uniqueness of deriving transformations, which are not already ruled out by the refined uniqueness theorem, can be realized.
We adapt a construction by Comer (1983) for polygroups to define the wreath product of the dual frames of two distributive quasi relation algebras satisfying certain conditions and show that it is itself a frame. Frames play a role analogous to that of atom structures for relation algebras. After introducing the notion of a frame network, we establish a correspondence between frame networks satisfying certain conditions and representability of finite distributive quasi relation algebras. Next we describe a frame network for the wreath product of two finite representable distributive quasi relation algebras that satisfies the aforementioned conditions, as well as additional conditions, and use this to conclude that the complex algebra of the wreath product is a representable distributive quasi relation algebra. Thus, our construction provides a method for obtaining representable DqRAs from certain finite DqRAs that are already known to be representable.
Benjamin Bergougnoux, Vera Chekan, Giannos Stamoulis
For a graph $G$, the parameter treedepth measures the minimum depth among all forests $F$, called elimination forests, such that $G$ is a subgraph of the ancestor-descendant closure of $F$. We introduce a logic, called neighborhood operator logic with acyclicity, connectivity and clique constraints ($\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ for short), that captures all NP-hard problems like Independent Set or Hamiltonian Cycle that are known to be tractable in time $2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$ and space $n^{\mathcal{O}(1)}$ on $n$-vertex graphs provided with elimination forests of depth $k$. We provide a model checking algorithm for $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ with such complexity that unifies and extends these results. For $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{k}$, the fragment of the above logic that does not use acyclicity and connectivity constraints, we get a strengthening of this result, where the space complexity is reduced to $\mathcal{O}(k\log(n))$. With a similar mechanism as the distance neighborhood logic introduced in [Bergougnoux, Dreier and Jaffke, SODA 2023], the logic $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ is an extension of the fully-existential $\mathsf{MSO}_2$ with predicates for (1) querying generalizations of the neighborhoods of vertex sets, (2) verifying the connectivity and acyclicity of vertex and edge sets, and (3) verifying that a vertex set induces a clique. Our results provide $2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$ time and $n^{\mathcal{O}(1)}$ space algorithms for problems for which the existence of such algorithms was previously unknown. In particular, $\mathsf{NEO}_2[\mathsf{FRec}]$ captures CNF-SAT via the incidence graphs associated to CNF formulas, and it also captures several modulo counting problems like Odd Dominating Set.
Bisimulation is a concept that captures behavioural equivalence of states in a variety of types of transition systems. It has been widely studied in discrete-time settings where a key notion is the bisimulation metric which quantifies "how similar two states are". In [ 11], we generalized the concept of bisimulation metric in order to metrize the behaviour of continuous-time Markov processes. Similarly to the discrete-time case, we constructed a pseudometric following two iterative approaches - through a functional and through a real-valued logic, and showed that the outcomes coincide: the pseudometric obtained from the logic is a specific fixpoint of the functional which yields our first pseudometric. However, different from the discrete-time setting, in which the process has a step-by-step dynamics, the behavioural pseudometric we constructed applies to Markov processes that evolve continuously through time, such as diffusions and jump diffusions. While our treatment of the pseudometric in [11] relied on the time-indexed Markov kernels, in [ 8 , 9, 10 ], we showed the importance of trajectories in the consideration of behavioural equivalences for true continuous-time Markov processes. In this paper, we take the work from [11 ] further and propose a second behavioural pseudometric for diffusions based on trajectories. We conduct a similar study of this pseudometric from both the perspective of a functional and the viewpoint of a real-valued logic. We also compare this pseudometric with the first pseudometric obtained in [11].
Victor Barroso-Nascimento, Joaquim T. Waddington, Elaine Pimentel
We investigate the relationship between base-extension semantics, Beth semantics, and Prawitz's ecumenical logic. We first present a base-extension semantics for the propositional fragment of Prawitz's system and prove that it is sound and complete. The semantics interprets intuitionistic and classical operators directly within a common proof-theoretic framework, without reducing the classical operators to their intuitionistic counterparts by means of a translation. We then analyse the effect of incorporating Beth-style clauses into base-extension semantics. When arbitrary bases are admitted and $\bot$ is governed by atomic explosion, these clauses trivialise. By contrast, when $\bot$ is treated as a basic sentence and attention is restricted to consistent bases, the Beth-style clauses for atoms and disjunction characterise, respectively, classical atoms and classical disjunction in Prawitz's system. We also obtain equivalent, path-independent formulations of the classical clauses for atoms, disjunction, and implication. These results reveal that the consistency constraint is not merely a technical restriction: within base-extension semantics, it transforms clauses originally associated with intuitionistic semantics into semantic characterisations of classical operators.
Order maintenance asks for a data structure that keeps a sequence of elements under insertions and deletions and tells which of two elements comes first. We give an algorithm, assembled from published components, that performs each operation in worst-case constant time, and verify it in Lean 4. The algorithm is a program for a random-access machine deeply embedded in Lean, whose interpreter counts every instruction. We prove that the program answers every query as a simple reference specification does, that each operation takes at most a fixed number of steps, independent of the number of elements and of the history, and that after $t$ operations no value it has computed has more than $O(\log t)$ bits, so it runs unchanged on a machine with words of that size. A verified translation that preserves step counts exactly connects the high-level proofs to the machine program, so the interpreter is the only cost model to trust. An unverified native implementation shows the algorithm's practical cost.
Confluence is a fundamental property of computation which implies that the nondeterminism of a system does not affect its outcomes. A key concept of confluence research in rewriting theory is the notion of critical pairs which captures the potential local sources of non-confluence. In this paper, we lift the definition of higher-order critical pairs to a more expressive class of higher-order rewrite systems. Thereby, we facilitate confluence analysis of rewrite systems which can express complex one-step computations as well as program transformations from functional programming.
A depth lower bound for ReLU networks asserts that every shallower network errs on some input; we ask when a weak theory can prove such a bound so that an error can be computed. For the exact computation of $\max(x_1,\ldots,x_n)$, recent work shows two hidden layers suffice with unrestricted rational weights. By contrast, Haase, Hertrich and Loho (ICLR 2023) proved that integer weights require depth logarithmic in $n$, and Averkov, Hojny and Merkert (ICLR 2025) extended the bound to nonbias weights whose denominators are powers of a fixed integer not divisible by a prime $q$. With integer weights the bound is sharp: the classical balanced construction has depth $\lceil\log_2 n\rceil$. For each fixed $q$ and depth cap $K$, we prove this known bound in $\mathbf{VTC}^0$, the bounded-arithmetic theory of uniform constant-depth threshold computation, together with a refuter that is itself such a computation and whose correctness the theory proves. Given a network with at most $K$ hidden layers, nonbias weights whose reduced denominators avoid $q$, arbitrary rational biases and $n>q^K$ inputs, the refuter returns a rational input of polynomial length on which the network errs. The proof makes the obstruction finite: an iterated intersection product of piecewise-linear functions is divisible by $q$ for the network but not for the maximum, so one of finitely many test points exposes the error. By witnessing, provable refutation corresponds to a provably correct refuter, and provable existence of a certified network to a provably correct constructor. On the construction side, we introduce certificates that label each maximum gadget by the inputs it aggregates; with them the theory verifies the balanced construction, which meets the refuter at the sharp threshold $n\le2^K$, and a rational family of polynomial description length and depth $O(\log n/\log\log n)$ built from known depth-two blocks.
We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.
We introduce partial Markov categories as a synthetic framework for synthetic probabilistic inference, blending the work of Cho and Jacobs, Fritz, and Golubtsov on Markov categories with the work of Cockett and Lack on cartesian restriction categories. We describe observations, Bayes' theorem, normalisation, and both Pearl's and Jeffrey's updates in purely categorical terms.
Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.
Quantifier shifts are one of the oldest proof methods, but they are orthogonal to the cut free format: They can shorten proofs non-elementarily. (The proof is based on the sequence of proofs exhibiting a non-elementary difference between proofs with cuts and cut-free proofs by Orevkov). The cost is, however, that those proofs are globally sound but locally unsound. (Their subderivations might be unsound in contrast to the Hilbert concept of proof). In non-classical logics these calculi are only sound when all quantifier shifts are added. This characterizes all intermediate logics where Skolemization and the epsilon calculus is conservative (in contrast to the epsilon theorem which holds only for finite-valued Goedel logics).
Data systems operating under persistent legal, institutional, and analytic disagreement require shared reference without presupposing agreement about interpretation. This paper investigates identity preservation under transformation, building on the conditional neutrality result of Neutral Substrates (arXiv:2601.14271). We pair candidate identity bases with families of record transformations and classify each family as preserving, breaking, neutral, or inapplicable for a basis. Using invariant-defined identity bases and explicit effect models, we derive and certify six classification cells in Lean 4 for scope decomposition, rule refinement, and forking. The derivations show how classifications depend on field granularity, admissible transformation steps, and explicit continuity warrants. We also characterize the identity relations generated by invariant-preserving steps. Two bases generate equal relations exactly when they agree on the preservation of every admissible step in a shared comparison domain, and a single separating step witnesses a difference. The formalization makes identity claims auditable, provides testable conditions for systems that transform records, and exposes the assumptions behind each classification. The results are conditional on the declared bases, models, and warrants, whose adequacy for particular referents requires independent justification.
Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.
Diaconescu's theorem derives excluded middle from the axiom of choice, using propositional extensionality. We show that in dependent type theory without propositional extensionality, global choice alone does not imply excluded middle. We consider extensional Martin-Löf type theory with an impredicative universe of propositions included in the universe of types, extended with a global choice operator. We construct a consistent model of this type theory and show that the model refutes excluded middle and propositional extensionality. The model is built from staged sets, sets whose elements appear at stages of a well-order. It further validates proof irrelevance, inductive families, quotients with soundness, and a cumulative hierarchy of universes, which together cover a large fragment of the type theory of the proof assistant Lean. Even together with these features, global choice does not imply excluded middle.
We study algebras for the $\mathbf{BM}$-, $\mathbf{BI}$-, and $\mathbf{BMI}$-fragments of combinatory logic, where $\mathbf{B} xyz \to_{w} x\left(yz\right)$, $\mathbf{M} x \to_{w} xx$ and $\mathbf{I} x \to_{w} x$. We prove that every finite $\mathbf{BM}$-algebra $\mathcal{A}$ contains an element $Y$ satisfying $Yx = x\left(Yx\right)$ for all $x\in A$. Moreover, a single closed $\mathbf{BM}$-term represents such an element in every finite $\mathbf{BM}$-algebra. On the other hand, we show that there exists an infinite $\mathbf{BMI}$-algebra with no such element. Consequently, the variety of $\mathbf{BM}$-algebras is not generated by finite $\mathbf{BM}$-algebras. We also characterise finite $\mathbf{BI}$-algebras as finite semigroups with two distinguished left units $B$ and $I$, and finite $\mathbf{BMI}$-algebras as finite idempotent semigroups with three distinguished left units $B$, $M$ and $I$.
The logic KL$_1$ of Evans, Sergot and Stephenson formalizes Kant's rules as conditional imperatives $B \square\to C$ and permissives $B \diamond\to C$ over acts. Its consequence relation is operational: a rule follows from a set of rules when adjoining it leaves the set of outcomes unchanged for every input. The authors proved their calculus sound and conjectured that it is complete. We show that the conjecture fails: for distinct atoms $b,c,d$ the rules $\top \diamond\to b \lor d$, $b \diamond\to c$, $d \diamond\to c$ and $c \square\to b \lor d$ entail $\top \diamond\to c$, which is not derivable. Non-derivability is proved by an invariant that holds at every derivation depth and for arbitrary intermediate atoms. The obstruction is the side condition of may-trans, which requires each new act to bring with it a single intermediary act. Replacing it by a disjunctive side condition yields may-trans-disj, a strict generalization from which the original rule is derivable. Using a local characterization of entailment, we prove the repaired calculus sound for arbitrary sets of rules and complete for finite ones, and we show that, with finite inputs, completeness cannot be extended to infinite sets. The main results on KL$_1$ are formalized in Agda. For KL$_2$ we observe that the published reduction to KL$_1$ passes through infinite rule sets; re-establishing the decomposition for finite rule sets, we prove that KL$_2$ with the disjunctive rule is sound and complete for finite sets of rules. We close with remarks on KL$_3$ and on the significance of completeness for the relation between the operational and the inferential questions of Kant's logic.
We study the expressive power of First-Order Logic (\FO) over (unordered) infinite trees, with the aim of identifying robust characterisations in terms of branching-time specification formalisms. While such correspondences are well understood in the linear-time setting, the branching-time case presents well-known structural challenges. To this end, we introduce two classes of hesitant tree automata and show that they capture precisely the expressive power of two branching-time temporal logics, namely \PolPCTL and \CTLsf, both of which have been previously shown to be equivalent to \FO over infinite trees. These results provide uniform automata-theoretic characterisations and yield a natural normal form for the latter in terms of a new fragment of \CTLs called \PolCTLs. As a consequence, we identify a fundamental limitation of \FO in this setting: along each branch, it can express only properties that are either safety or co-safety, thereby revealing a sharp expressive boundary for first-order definability over infinite trees.
On the theoretic analyses on transforms, they mainly focus on the computability analysis, such the Turing-completeness of unbounded precision transformers, the advantage of parallelizability of unbounded precision transformers and the limitations of bounded precision transformers. This paper give transformers an algebra for reasoning, which relies heavily on the functional decomposition results of transformers. This algebra uses functional decompositions as atomic actions, includes sequential composition and parallel composition, recursion for feedback and abstraction for hidden layers. As we know, it is the first attempt to model transformers logically and can be used to verify the correctness of transformer based applications.
We present Unit, a type checker for dependent type theory with a module system in the tradition of Automath and a uniform treatment of definitions. There is no unification, no instance search, no tactics and no unfolding heuristic, so the work of checking can be observed and compared with the informal proof. With Unit we have checked a model of univalent type theory, synthetic algebraic geometry up to Chatelet's theorem, and synthetic Stone duality with its cohomology, and results on finite free resolustions. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.
Optimizing expected rewards and reachability probabilities in parametric Markov chains (pMCs) is central to the analysis and synthesis of probabilistic systems with loops. While traditional symbolic synthesis approaches--such as parameter lifting and rational function generation--suffer from scalability bottlenecks, gradient-based optimization emerges as an effective alternative. However, existing gradient-based techniques still rely on symbolic gradient computation--such as solving large linear systems--over the global state space, inheriting scalability limits. Finite-horizon approximation is possible but introduces uncontrollable bias. In this paper, we introduce a scalable Monte Carlo gradient estimator based on a measure-theoretic generalization of the log-derivative trick. We prove that our estimator provides unbiased gradient estimates under almost-sure termination and standard regularity conditions. Crucially, our method avoids global state-space materialization and linear system solving entirely: it operates purely along sampled trajectories, requiring only black-box evaluations of local transition probabilities (or densities) and their derivatives. Unlike existing pMC techniques that are fundamentally restricted to finite discrete systems, our measure-theoretic framework naturally extends to continuous and general $σ$-finite state spaces. Empirical evaluations on synthetic discrete pMCs and continuous-state case studies demonstrate that our method scales to state spaces far beyond the reach of existing solvers, significantly reducing execution time without introducing bias.
Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.
The fibrational framework of Licata, Shulman, and Riley gives a uniform account of substructural and modal logics for single-conclusion judgments. This thesis extends it to a multiple-output setting in which cartesian resources may be used freely, while linear resources occur exactly once on either side of the turnstile. Judgments are indexed by descriptors: directed acyclic graphs generalizing the tree-shaped expressions of the original framework. Descriptor $2$-cells encode structural transformations, and explicit gates provide weakening, contraction, coweakening, and cocontraction at linear modes. We define a sequent calculus generated by two connectives, $F$ and $U$. We prove identity, invertibility, and cut admissibility. The mode and type theories present linear-non-linear $2$-polycategories, and the projection is a local discrete fibration and a fibration, with opcartesian lifts for one-output base morphisms. Two adequacy results validate the framework: its cartesian fragment recovers the Licata--Shulman--Riley calculus, and its purely linear fragment presents classical multiplicative linear logic. Finally, we relate indexed and fibrational semantics. After developing representability correspondences for multicategories and polycategories, we establish an equivalence between multi-indexed categories over a fixed representable base and multicategorical opfibrations over it, together with its biclosed bifibrational version. We also give a one-way construction from planar poly-indexed data to a planar polycategory.
We study completely normal elements of $\mathbb{F}_{q^n}$ over $\mathbb{F}_q$, that is, elements that are normal over every intermediate field, through partial Lagrange resolvents. In these coordinates, complete normality splits into independent components, in a way closely related to Hachenberger's decomposition theory. Our main tool is a structure theorem for the components; together with a finite computation, it shows that every component has weight (the sum of the probabilities that its conditions fail) at most $3/4$, uniformly in $n$. Combined with the classical character-sum method, this gives an explicit sufficient criterion for the existence of a primitive completely normal element. We verify the criterion for all $n>q$ except $70$ pairs $(q,n)$, which we settle with explicit elements found by computer. Since the case $n\le q$ is due to Garefalakis and Kapetanakis, this confirms the conjecture of Morgan and Mullen (1996) that every $\mathbb{F}_{q^n}$ contains a primitive element that is completely normal over $\mathbb{F}_q$. The same estimates give two further results. First, Hachenberger's conjectured lower bound $(q-1)^{n'}q^{(p^a-1)n'}$ for the number of completely normal elements, where $p$ is the characteristic and $n=p^an'$ with $p\nmid n'$, holds for all pairs $(q,n)$; it was known for regular pairs. Second, primitivity and complete normality are asymptotically independent: as $q^n\to\infty$, the number of primitive completely normal elements is $(1+o(1))\,\varphi(q^n-1)/(q^n-1)$ times the number of completely normal elements (for fixed $n$ this was known). Our arguments for $n>q$ and for both further results, including every computer-assisted step, are formalised in Lean 4 with Mathlib; the formalisation takes the case $n\le q$ and an explicit bound of Rosser and Schoenfeld as axioms and relies on Lean's compiler and interpreter for the large computations.
Aditya Ranjan Jha, Jason Zhijingcheng Yu, Umang Mathur, Prateek Saxena
Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is thus a global property, determined by interactions between components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the rest of the system exists. The check produces a summary type that captures the communication behaviour left for future compositions. To reduce annotation burden, Pact infers types by abstracting payload values while preserving communication, timing, control, and fairness. These inferred types are optimal for the checker: whenever some checker-accepted types can prove compatibility, the inferred types can prove it as well. Type inference and type checking are decidable, and compatibility is decided by a sound and complete algorithm. We implement Pact by extending the Anvil compiler and evaluate it along five dimensions: detecting communication errors in incremental design, expressiveness on ten clock-cycle-accurate translations of open-source hardware IPs, compatibility-checking time, generated hardware overhead, and annotation burden. Pact expresses realistic protocols and verifies all ten benchmarks in reasonable time.
We present Alaska's ranked-choice elections as a case study in Formally Verified Democracy, a program to establish election results through formally checked proofs. We formalize an interpretation of Alaska's tabulation rules in Lean, verify its implementation, and prove election-specific results. Across 115 ranked-choice contests in Alaska since 2022, we identify 75 ballot records across 10 contests that were counted differently from this interpretation by a program reproducing the published results, without changing any winners. We trace these differences to overvotes and duplicate rankings and examine their legal justification, showing how formal verification can expose consequential choices in translating election law into software.
This note documents the specification of normal forms in cubical type theory. The definition is already present in the proof of normalization for cubical type theory, but we present it in a more traditional style explicitly for reference.
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.