ABSTRACT. We introduce a new family of benchmarks for the problem of diagrammatic equiva- lence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances. We evaluate these benchmarks on state-of-the-art auto- mated theorem provers and SMT solvers, highlighting the impact of encoding choices on solver performance.

ABSTRACT. We provide a translation from problems of the Thousands of Problems for Theorem Provers (TPTP) Problem Library to Lean expressions. This makes the TPTP Problem Library available as a benchmark set for proof automation tactics inside Lean. We evaluate our tool by comparing its performance with that of the Lean compiler on equivalent inputs. Furthermore, we use our tool to compare different Lean proof automation tactics.

ABSTRACT. We report on our efforts to translate HOL-Light theorems on HOL-Light types/functions into Rocq theorems on Rocq types/functions. To this end, we developed in Rocq tactics to automate the proofs required for replacing a HOL-Light inductive type or recursive function definition by an equivalent but more idiomatic one in Rocq. We also explain how we replaced the definition of real numbers, as well as a number of mathematical notions like R^n spaces and the definition of limit, hence providing to Rocq users many definitions and theorems in logic and analysis that had not been formalized in Rocq before.

ABSTRACT. We identify common challenges and requirements for verifying proofs of 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 a large part of the calculus EP for higher-order logic, and integrate it into the automated theorem prover Leo-III, making it the first automated theorem prover for higher-order logic whose proofs can be independently checked and reused across systems. This uncovered and fixed several bugs in Leo-III.

ABSTRACT. Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean 4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks -- recurrent networks that store patterns as stable states -- and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity -- convergence to a \emph{unique} stationary distribution -- via a new formalization of the Perron--Frobenius theorem.

ABSTRACT. We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform axiomatic foundation for specifying and verifying programming languages and security protocols. We expose a DSL for users to define languages and protocols as many-sorted signatures, specify the relevant domain-specific axioms, and reason about program executions or protocol runs. We provide a machine-checked proof of its soundness theorem and showcase the framework's versatility through several applications: an imperative programming language for code verification, a BAN logic and an epsitemic logic used for security protocols, and the modal system S5. We have designed our formalization to be intrinsically sorted, that is, well-sorted formulas in the base language are well-typed terms in Lean. Thanks to intrinsic sorting, all domain specific applications can be easily embedded in our framework via the DSL, at no additional syntactic overhead required for the user to prove.

ABSTRACT. Pattern-matching is the primary programming construct used to analyze the contents of algebraic data types in statically typed functional languages. Additionally, dependent types allow us to benefit from very precise information about data being processed. However, pattern-matching on dependent types turned out to raise surprisingly complex challenges, that have required more than two decades of intensive research to produce current implementations in Agda, Epigram and the Equations plugin of Rocq. Another popular tool among Rocq users is the historical inversion tactic which solves many use cases at the cost of a loss of control over the form of the programs obtained and some reliability issues. Both approaches in Rocq rely on intermediate equalities to produce a well-typed term in the underlying type theory, many of which turn out to be unnecessary. Alongside those tools, we believe that there is room for a complementary minimalist approach based on recent improvements of small inversions that generates explicit terms that are more readable and explainable. We present here this approach and its current automation implemented in MetaRocq.

ABSTRACT. We present a solver for $N$-Queens Completion puzzles in Lean~4 that applies collaborative neurodynamic optimization algorithms over discrete Hopfield networks or Boltzmann machines. We prove the correctness of the translation from the puzzles to the networks, and implement the algorithms that search those networks inside the prover. We report experiments on a corpus of completable and blocked boards, against a backtracking baseline proved to return only completions.