ABSTRACT. While the ITP world is getting dominated by Lean, on the AI side, we are just starting to understand the possibilities that coding agents offer. They can not only write formal proofs, write Lean tactics (which write formal proofs) but even write a brand new ITP from scratch. We will take a look at a particular experiment of human written kernel & axioms, and AI-written proofs & automation.

ABSTRACT. Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.

ABSTRACT. The interpretation of mathematical expressions is inherently context-sensitive as it depends on (at least) local notations and typing information. Nonetheless, it is desirable to have parsers that can handle as much as possible in a single context-free pass.

We present a set of rules for context-free parsing of expressions in a way that covers many use cases correctly and makes it easy elaborate context-sensitively in a subsequent type-checking phase. While far from sufficient for processing all expressions found in informal mathematical texts, it is a reasonable trade-off for implementations of formal languages. We have implemented our parser as a part of the UniFormal language.

ABSTRACT. Natty is a proof assistant based on controlled natural language and higher-order logic. An input file for Natty is written in a controlled natural language called N that is designed to look like ordinary mathematical writing. The input can contain axioms, definitions, and theorems with or without proofs. Natty translates the input into a series of formulas of higher-order logic and then attempts to prove them using an embedded automatic prover based on higher-order superposition. Alternatively, Natty can export the formulas to files in the standard THF format. A novel feature is that Natty automatically infers the hierarchical structure of proofs, which makes the input especially readable. The system includes a mathematical library of over 230 theorems that starts with the Peano axioms and develops the natural numbers, integers and rationals, proving 5 of Wiedijk's well-known 100 theorems.