MALINCA

Proof Assistant Assistants: From teaching Rocq to LLM-assisted proofs

Guillaume Baudart, Emilio J. Gallego Arias — Inria, CNRS

While Proof Assistants have been proven to be extremely helpful, they are also known for being extremely challenging to use, learn, and adapt to the large and diverse set of applicable use cases.

In the first part of this talk, we will present Flèche, a new document manager for the Rocq proof assistant that was originally designed for teaching Rocq. Flèche aims to make it easier to build enhanced proof assistants. It has been built taking into account extensive user and developer feedback, and provides a unique set of features and extensibility.

Flèche's aims are twofold: we want to provide a usable, production ready platform for people willing to extend proof assistants at the document level; while at the same time developing such document managers in a rigorous, scientific way.

In the second part, we will present specialized tools for LLM-assisted proofs. First, the petanque and rocq-mcp protocols, built on top of Flèche, enable the interaction between LLMs and the Rocq prover.

We can then design agents that leverage both natural language reasoning and interactive proof search to formalize mathematical proofs.

We also train specialized LLMs assistants to suggest tactics, search for relevant theorems, translate results from one proof assistant to another, or guide the interactions with these tools.

Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

Cyril Cohen — Inria

In this talk I present Trocq, a proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq interactive theorem prover, in the Rocq-Elpi meta-language.

This is a joint work with Enzo Crance and Assia Mahboubi.

Towards autoformalization of textbook mathematics with natural proof checking

Adrian De Lon — Mathematical Logic Group, University of Boon, Czech Institute of Informatics Robotics and Cybernetics

Textbook mathematics relies on context and implicit reasoning, presenting its arguments in a form optimizedfor human comprehension rather than formal verification. Formal systems, in contrast, demand explicit, step-by-step arguments in a rigid syntax, which contributes to the difficulty of formalization. To bridge this gap, we propose using a controlled natural language as an intermediate representation, augmented by automated theorem provers to verify human-sized proof steps. The design of this language draws both from practical experiences with proof vernaculars of interactive theorem provers and from techniques of formal linguistics. This approach aligns naturally with LLM-based autoformalization, exploiting the vast corpus of quasiformalist mathematical texts. By isolating essential mathematical content from incidental surface details, it opens a path towards systematic modelling and verification of textbook mathematics.

How can Machine Learning Help Mathematicians?

Amaury Hayat — École des Ponts, Institut Polytechnique de Paris

The advent of artificial intelligence raises an important question: Can AI assist mathematicians in solving open problems in mathematics? This talk explores this question from multiple perspectives. We will explore how different types of AI models can be trained to provide valuable insights into mathematical questions to recent progresses in the field of automated theorem proving.

Language and Mathematics in the Time of AI. Philosophical and Theoretical Perspectives

Juan Luis Gastaldi — ETH Zurich

Under the banner of Artificial Intelligence (AI), the past decade has witnessed a remarkable development of deep neural network techniques for data analysis, along with their increasing application across scientific disciplines, including mathematics. In this presentation, I will explore the philosophical implications of these developments and argue that they may yield new theoretical insights into the nature of mathematics. The path from philosophical to theoretical insights will be guided by the claim that, owing to the relative success of neural methods, natural language has become central to the computational treatment of mathematical content, forcing us to reflect on the implications of a distributional rather than an analytic approach to mathematics. After providing philosophical, historical, and epistemological perspectives on this problem, I will conclude by proposing some conceptual orientations for a distributional approach to mathematical contents, in line with ongoing theoretical efforts to develop a formal framework for extracting symbolic principles underlying textual corpora.

Organising large proofs: techniques, tools, and future

Georges Gonthier — Inria

Designing Interactive Partners for Proof

Andrew Head — University of Pennsylvania

Proof has a reputation for being hard to write and understand. What about the mediums for proof makes it so, and could we change it? In this talk, I share lessons learned from my group's work in the human-computer interaction (HCI) of proof and formalisms. I begin with a rich characterization of the modern UX of proof informed by a qualitative study of real work sessions of Rocq and Lean users. Then, I share ideas for how we might make proof more approachable, foregrounding my group's recent efforts to build tools that make notation more understandable and accelerate property-based testing. Along the way, I highlight strategies from our HCI work that have helped us gain insight into the realities of proof work and the effects of tools.

Flexiformal mathematics

Michael Kohlhase – FAU Erlangen-Nürnberg, Carnegie Mellon University

Introduction to Grammatical Framework

Inari Listenmaa – Chalmers University of Technology

Grammatical Framework (GF) is a framework for building multilingual grammar applications. It is based on the idea of a shared abstract syntax and mappings between the abstract syntax and concrete languages. GF's main components are a functional programming language and a resource library that contains the linguistic details of many natural languages.

In this talk, I will first give a high-level overview of the GF language and its previous applications, followed by a more detail-oriented tutorial. In case of further interest, I'm happy to provide an additional hands-on session after the official program.

Certifying the decidability of the word problem in monoids, at large

Assia Mahboubi – Inria

The word problem for monoids is a classic example of undecidability. However, many special cases of this general problem still defy comprehension (as of today). For instance, the word problem for one-relation monoids is one of the most fundamental open questions in combinatorial algebra. This talk will present a framework organizing the cooperation of an interactive theorem prover with an array of computer-algebra tools for exploring the decidability of the word problem in finitely presented monoids. This approach has been successfully applied to large, concrete examples from the literature, as well as on a database of one-million one-relation monoids. In particular, the huge size of this database induces some unusual considerations upon the formal verification, conducted using the Rocq Prover, so that its formal proof could be checked in a reasonable amount of time.

Joint work with Reinis Cirpons, Florent Hivert, Guillaume Melquiond, James Mitchell and Finn Smith

From informal to formal and back

Patrick Massot – Laboratoire de Mathématiques d'Orsay, Université Paris-Saclay

I will first discuss Verbose Lean, a teaching library where students use controlled natural language and custom automation to write proofs in Lean. The goal of this library is not to make it easy to write Lean code, the goal is to make it easy to transfer proving skills from computer to paper. This library shares many goals and solutions with the Rocq Waterproof library. Then I will discuss Informal Lean, a project with Kyle Miller to turn Lean files into interactive web pages in natural language where readers can choose the level of detail.

Waterproof: transforming a proof assistant into an educational tool

Jim Portegies — Eindhoven University of Technology

To help students with acquiring the skill of giving mathematical proofs, we developed the educational software Waterproof, which consists of a Rocq plugin and an extension for Visual Studio Code. Waterproof uses controlled natural language, and we try to bring writing proofs in Waterproof as close as possible to writing proofs on paper. In this talk I will discuss some of our design choices, some of the evaluations we have performed, and some preliminary work on using large language models to guide students through exercises.

Some remarks about machine learning and (un)natural proving

Josef Urban – Czech Institute of Informatics Robotics and Cybernetics

Human-readable Proof Documents and Embedded Sublanguages in Isabelle/Isar

Makarius Wenzel

Isabelle/Pure was originally introduced by Paulson (1986/1989) as a Logical Framework to specify object-logics declaratively, based on Higher-order Natural Deduction. Isabelle/HOL emerged soon as main object-logic and Isabelle application, with many tools for specifications and proofs written in Isabelle/ML.

Isabelle/Isar was added by Wenzel (1999) as a structured language for Human-readable formal proof documents: it works with Isabelle/Pure and regular object-logics. The proof language has been reworked over the decades, with notable extensions in 2015/2016, including the Eisbach language for Isar Proof Methods. Already, from the beginning, Isar had been accompanied by the Isabelle Document language, to write mathematical texts with high-quality typesetting in LaTeX.

So today we may see Isabelle as an agglomeration of many languages for different purposes, all integrated into a single System Framework in Isabelle/Scala. That includes the Isabelle/PIDE Prover IDE with parallel and asynchronous processing of formal documents, and the Isabelle build system (with its distributed cluster manager). Thus we can carry the weight and gravity of large proof documents, as e.g. seen in the Archive of Formal Proofs (AFP).