ABSTRACT. The starting point of this paper is a recent formal verification by Nipkow and Rau of an abstract inductive but not directly executable (i.e.\ recursive) version of Earley's recognizer. The aim of that work was a particularly simple, abstract formalization and stepwise refinement towards executability. We continue this work and refine it to an executable implementation together with a proof of the running time: cubic if the $n$-th element of a list can be accessed in constant time, and quartic if access takes linear time. We present the running time analysis with the help of a simple Big $O$ formalization.

ABSTRACT. A well-known folklore result about propositional logic is that transforming a formula in disjunctive or conjunctive normal form can lead to an exponential blowup of the formula size. We formalize this result in the form of two theorems in Isabelle/HOL and discuss the challenges we encountered.

ABSTRACT. We present initial work on formally verifying the core of the egg framework in Isabelle/HOL. The egg framework uses e-graphs to perform fast, extensible equality saturation. Congruence closure is a core technique in program analysis and program optimization, serving as a foundation for rewriting systems and enabling efficient reasoning in equational logic. Optimization techniques such as egg's deferred rebuilding mechanism, however, obscure the computation and thus reduce confidence in the results. In this work, we aim to provide a comprehensive, extensible formalization of egg's data structures and algorithms, with a focus on the correctness of deferred rebuilding. Ultimately, we seek to export a verified implementation to Standard ML, enabling trustworthy, executable equality saturation.

ABSTRACT. Standard logical foundations in theorem proving constrain the set of recursive functions that are directly expressible to avoid inconsistencies. However, this prevents us from expressing all Turing-complete computations via direct recursive definitions. We consider Grounded Arithmetic, a reasoning framework that avoids inconsistency from unconstrained recursive definitions by "dynamically type-checking'' terms. Using the formalization of GA in Isabelle/HOL, we prove three self-referential statements to be nonterminating computation: the Liar Paradox, the Truthteller sentence, and Curry's paradox. To do so, we model each statement in GA as a function taking a certain number of steps of computation, and metalogically derive a contradiction if these terms were to terminate. In turn, this allows us to show that these statements have no concrete value in our framework. Using our non-standard inference rules, terms with no concrete value cannot be used in a proof by contradiction, and thus are inert when reasoning about other computations. We then discuss the accessibility of our approach, and how it permits us to avoid common inconsistencies that would otherwise occur when removing constraints from direct recursive definitions in other formal systems.

ABSTRACT. Recent advances in expressiveness of the modal mu-calculus has prompted usage of a generalized Bekic principle with n variables for n>2. However, the only version of Bekic principle known to exist in mathematical literature is for n=2. Indeed, it is non-trivial to even state the principle precisely for more than 2 variables because of the recursive structure involved. This paper presents a precise mathematical statement and proof of the general Bekic principle for any positive n, as well as a mechanization of the proof in Isabelle. As an application, this result serves as a basis of a formal translation from sabotage game logic to recursive game logic, establishing equiexpressiveness to mu-calculus.

ABSTRACT. Mathematicians and computer scientists are increasingly using proof assistants to formalize and check correctness of complex proofs. This is a non-trivial task in itself, however, with high demands on human expertise. Can we lower the bar by introducing automation for conjecturing helpful, interesting and novel lemmas? We present the first neuro-symbolic lemma conjecturing tool, LEMMANAID, designed to discover conjectures by drawing analogies between mathematical theories. LEMMANAID uses a fine-tuned LLM to generate lemma templates that describe the shape of a lemma, and symbolic methods to fill in the details. We compare LEMMANAID against the same LLM fine-tuned to generate complete lemma statements (a purely neural method), as well as a fully symbolic conjecturing method. LEMMANAID consistently outperforms both neural and symbolic methods on test sets from Isabelle's HOL library and from its Archive of Formal Proofs (AFP). Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 28% (AFP) of the gold standard reference lemmas, 8-13% more than the corresponding neural-only method. Ensembling two LEMMANAID versions with different prompting strategies further increases performance to 55% and 34% respectively. In a case study on the formalization of Octonions, LEMMANAID discovers 79% of the gold standard lemmas, compared to 62% for neural-only and 23% for the state of the art symbolic tool. Our result show that LEMMANAID is able to conjecture a significant number of interesting lemmas across a wide range of domains covering formalizations over complex concepts in both mathematics and computer science, going far beyond the basic concepts of standard benchmarks such as miniF2F, PutnamBench and ProofNet.

ABSTRACT. Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for Isabelle/HOL. Given a challenging proof goal, the Abduction Prover constructs a proof script for the goal by identifying useful conjectures using abductive reasoning.

ABSTRACT. Large language models (LLMs) and proof assistants are in the early days of a fruitful marriage. LLM-based agents draft and mechanize, while the proof assistants patiently check the resulting proofs. We consider two aspects of safety when integrating agents with the Isabelle proof assistant. First, we survey different technological methods to isolating agents and restricting what they can do through Isabelle. Second, we discuss different agentic workflows and the degree of human intervention needed to assure the logical consistency of the resulting artifacts.