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. In this article, we present a formalization of a general many-sorted hybrid polyadic modal logic within the Lean proof assistant. We provide a machine-checked proof of its soundness theorem and demonstrate how specific formalisms can be derived as subsystems. To facilitate this, we implement a generic DSL that allows users to define many-sorted signatures using intuitive notation. We showcase the framework's versatility through several applications: an SMC-like language for program analysis, a logic for security protocols, and the modal system S5.

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 translation from the puzzles to the networks correct, 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.