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. While datasets of mathematical objects may provide precomputed properties of said objects and thus save the user from expensive computations, verifying their correctness could be as expensive, as in the worst case we might have to recompute from scratch. Often we can mitigate this problem by providing certificates which make it possible to verify the properties efficiently. Such certificates may also help import the objects from the dataset into a proof assistant.

We have designed a certificate for the automorphism group of a graph that efficiently certifies the fact that a given permutation group is the full automorphism group of a given graph. We computed the certificates for the combined censuses of connected cubic vertex-transitive graphs on up to 1280 vertices by Potočnik, Spiga and Verret, and of connected cubic symmetric graphs on up to 2048 vertices by Conder. The censuses are available in the DiscreteZOO database. Our certificates can be used to verify further symmetry properties of the graphs, such as their vertex- and arc-transitivity.

ABSTRACT. We consider the problem of identifying subsets of variables that are likely to participate in an underlying (possibly unknown) relationship within a mathematical database. We treat each variable as a target and assess the predictive relevance of all others using a diverse collection of machine learning algorithms. Aggregating multiple measures of predictive importance yields a weighted network of pairwise dependencies among variables. We conjecture that groups of variables with high mutual predictive importance correspond to candidates for meaningful mathematical relationships. We test this hypothesis on a curated subset of integer sequences from the OEIS with known interdependencies. Our results show that when algorithms are trained on sufficiently long prefixes of the sequences, the method identifies variables involved in known relationships and suggests candidate relationships, achieving an Area Under the Precision–Recall Curve (AUPRC) that is more than four times that of a random baseline.

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. Mathematical expressions may contain undefined terms, and mathematicians employ a lot of ingenuity to handle them: for example, manipulating limits before they are shown to exist -- without introducing inconsistencies -- or yet avoiding redundant existence condition checks in clever ways. Teaching how to do so is an important topic in undergraduate math, as students should quickly become familiar with these methodologies, and capturing them formally is complex. Whereas ad-hoc logics have been developed for this task, interactive provers and mathematical tools that we would also like to employ in education are based on a total logic, where undefined terms can only be encoded in a non-totally satisfactory way. In this paper, we implement a toolbox to encode partial terms, strict functions and predicates in type theory, partially automating the reasoning about definedness. Moreover, we capture some of the ingenuity of mathematicians in postponing and minimizing the need to check terms to be defined.

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.

ABSTRACT. Mathswitch is an open-source project that imports mathematical concept records from sources such as WikiData, Wikipedia, MathWorld, Encyclopedia of Mathematics, nLab, ProofWiki, and Agda-Unimath, and links records that refer to the same concept. It does not reorganize or redefine the imported content; each source retains its own structure. The current focus is on importing high-quality concept data from WikiData and the resources it links to, with plans to expand to further sources and better concept linking. Because the concept set is approximated through queries over WikiData's collaboratively edited graph, the imported data is noisy: some items are non-mathematical, while others are ambiguous. In this paper, we test whether a voting ensemble of LLM judges can filter this noise. We evaluate it on WikiData items with known MathWorld identifiers as a positive control, and examine how classification changes when database identifiers are removed from context. We then inspect the cases where the judges disagree with MathWorld and group these disagreements into three categories (degenerate descriptions, narrow scope bias, and editorial-scope mismatches) that suggest different remediation strategies.