ABSTRACT. What happens when you put millions of dollars in a computer program that no one can stop or modify? You get Ethereum smart contracts — and a very strong motivation for formal verification. Interactive and automated theorem provers are not just tools of academic curiosity: they are increasingly applied to real-world critical software. In this talk, I will present act, a formal verification framework that brings the power of proof assistants to Ethereum smart contracts via SMT solvers. At its core, act is a typed intermediate specification language with mechanised meta-theory (type safety, proved in Rocq). It sits between and is connected to source languages (like Solidity and Vyper) and proof assistants (Lean and Rocq). With act, one can formally specify smart contracts to state and prove correctness invariants in proof assistants. Additionally act leverages SMT solvers to automatically prove that the economic incentives encoded in the contract are aligned with honest behaviour.

ABSTRACT. Autoformalization can now produce machine-checked mathematical developments, but the resulting proofs can be too verbose to read as mathematics. To address this issue, we introduce proof distillation for Felix, a proof assistant for natural formalization. Starting from a semi-autonomously generated Felix formalization of Munkres’s Topology through Urysohn’s lemma, we study automated proof refactoring that preserves verifiability while removing locally superfluous proof detail. As a first step towards readable proofs, our preliminary experiments reduced the development from about 64,000 to 26,500 lines. This motivates a first design space for proof refactoring in ATP-backed natural formalizations, where proof distillation should not only preserve correctness, but also readability, proof structure, and traceability to the source. We describe our current workflow, illustrate recurring distillation patterns, and outline immediate directions for evaluating distilled proofs beyond line count. The broader aim is to turn autoformalized mathematics into material that can be read, debugged, and extended, not merely verified.

ABSTRACT. Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory demand of proof checking without altering overall size. Metamath serves as a prime case study for this approach: its verification architecture requires proof steps to be ordered in a manner that prioritises algorithmic efficiency over readability. In this paper, we introduce algorithms to minimise both peak and cumulative memory consumption, applying the latter as a novel proxy for sustained human cognitive effort. We achieve this by representing proofs as directed acyclic graphs and modelling their execution as a pebbling game. Finding an optimal ordering via brute force is computationally infeasible, so we use heuristics to provide approximations. We apply these algorithms across Metamath's ZFC set theory library and present case studies demonstrating how automated reordering systematically improves the presentation of formal mathematics.

ABSTRACT. To be effective, learning support systems need to be able to adapt to the individual learner or cohort, just as good teachers do. A clear and reliable idea of which parts of the domain of discourse any given learner already knows how much about is central to tailoring learning services to be useful and successful. In this paper, we describe and discuss the three different approaches to learner modelling used in the ALeA system, a learning platform in development and in use at FAU. This includes the structure of the underlying model and its foundations in didactics research as well as the update dynamics of each approach. We also present an empirical evaluation of the three approaches with each other and against performance in weekly quizzes. We conclude with a discussion of how this framework of evaluating learner modelling design choices can also function as a data-driven testing ground for additional learner model features.

ABSTRACT. Linking semantic concepts and natural language is the key to a variety of applications in natural language processing (NLP). In this report we discuss on-going work to build a lexical resource that links concepts to their renderings in natural language. Concretely, we present a specification format for such resources in sTeX that allows us to export them as a GF lexicon to be used in grammar-based NLP applications.

ABSTRACT. AI-assisted formal mathematics needs an audit interface between generated objects, proof-assistant checks, finite evidence rows, advisory agents, and human publication decisions. We present a compact publication-coordinate design pattern for that interface. A generated item is not promoted directly from model output to publication claim; it is first assigned to one of six roles and then to the strongest coordinate justified by finite records. The presentation-only contribution is the interface and its bounded checker contract, illustrated on a theory-to-paper pipeline case from the newmath/automath workspaces.

ABSTRACT. Problems complete for the existential theory of the reals ($\exists \mathbb{R}$) arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based approach for solving satisfiable instances of $\exists \mathbb{R}$ whose solutions correspond to realizable geometric configurations. Our method encodes an underapproximation of a geometric problem as a SAT instance over order types. Since almost all order types are unrealizable, naive search is infeasible. We guide the search toward realizable order types using diversity-driven sampling, partial realizability feedback, and a novel flippability heuristic that passes only limited information between components. We apply our method to discrete geometry problems and resolve an open problem by showing that the largest set of points avoiding empty convex hexagons and convex heptagons is of size 23.

ABSTRACT. We present Vampire Guide, a web platform for learning and teaching first-order theorem proving with the Vampire prover. Our plat- form addresses two goals: making modern automated reasoning easier to use, and supporting direct education of automated reasoning. Vam- pire Guide includes a custom WebAssembly deployment of Vampire for browser-based usage. It supports both automatic runs and interactive proof-search exploration with or without a visualization of given clause selection, helping interested users to understand how superposition-based proof derivations develop and why proof attempts succeed or fail. We po- sition our work both as an extension of the Vampire ecosystem and as an experience report on communicating automated reasoning to broader scientific and educational communities. Vampire Guide is already used for teaching at TU Wien and also hosts lecture content for this purpose.

ABSTRACT. In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems such as Aletheia. A Planner agent maintains a compact Whiteboard scratchpad and an unbounded Repository of intermediate findings, and decomposes mathematical work into parallel Workers.

OpenProver is fully open-source, supports reproducible evaluation through automatic formal verification of generated proofs, and provides an interactive terminal interface for human-guided proof search. In interactive mode, OpenProver allows the human operator to monitor and steer the proof search process, motivated by the established human-AI synergy in the field of interactive code generation.

To showcase the potential for quantitative ablation experiments enabled by automatic formal verification, we evaluate OpenProver on ProofNet and compare it with a simple baseline. OpenProver is publicly available at github.com/LeanTreeAnonymized/OpenProver.

ABSTRACT. We present higher-order versions of ENIGMA and Deepire, the two prominent learning-guided reasoning systems extending saturation-based automatic theorem provers E and Vampire, respectively. We evaluate these on a large Isabelle/HOL corpus, which emulates their use in Sledgehammer, and observe consistent improvement. Stress-testing the Sledgehammer export revealed several bugs, both in the provers and in Sledgehammer itself, which were all fixed for the final evaluation.

ABSTRACT. This project paper reports on an openly available prototype framework for Isabelle-based machine-learning research. The framework combines three components: extraction of stepwise proof traces from Isabelle theories, programmable interaction with Isabelle through Scala and Python REPLs, and a modular evaluation loop for training and testing proof-step predictors. Applied to the Archive of Formal Proofs (AFP), the extractor produces 241,126 JSON files from the January 2026 AFP snapshot. The extracted data is used to train and fine-tune language models, including T5 variants and a fine-tuned Gemma~3n model. The framework also serves to evaluate frontier-model backends via a REPL-based depth-first proof search. The experiments reproduce the expected advantage of domain-specific fine-tuning over training from scratch and show that the framework supports both local and API-based model backends. In proof completion on short AFP proofs, stronger frontier and fine-tuned models outperform the small T5 baselines, while Sledgehammer remains the strongest overall baseline. The contribution of the paper is primarily infrastructural: an open Isabelle environment for reproducible data extraction, model training, and multi-backend evaluation.