CHANGE Seminar

An Invitation to Blueprint-Driven Formalisation of Mathematical Research in Lean

Pietro Monticone

University of Trento

February 11, 2025

Outline

Outline

0. Preliminaries

  • Premises
  • Resources

1. What?

  • Context
  • Definitions

2. Why?

  • Motivation

3. How ?

  • Theory
  • Practice
  • Logistics

4. Future

5. Proposal

6. Discussion

Preliminaries

Premises

  • Philosophical disclaimer
  • Epistemic disclaimer
  • Deontological disclaimer
  • Non-contents
  • Distinctive features

Resources

Input

  • Literature
  • Personal experience
  • Expert consensus
  • Previous CHANGE seminars
  • Questions and requests

Output

  • Slides
  • Repository

What?

Context

It will hardly be possible to end controversies and impose silence on the sects, unless we reduce complex arguments to simple calculations, [and] terms of vague and uncertain significance to determinate characters. […] Once this has been done, whenever controversies arise, there will be no more need of a disputation between two philosophers than between two accountants. It will in fact suffice to take pen in hand, to sit at the abacus, and—having summoned, if one wishes, a friend—to say to one another: ‘let us calculate’ [calculemus].” — Gottfried Wilhelm Leibniz (1688)

Context

The development of mathematics toward greater precision has led, as is well known, to the formalisation of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. The most comprehensive formal systems that have been set up hitherto are the system of Principia Mathematica on the one hand and the Zermelo-Fraenkel axiom system of set theory […] on the other. These two systems are so comprehensive that in them all methods of proof used today in mathematics are formalized, that is, reduced to a few axioms and rules of inference. — Kurt Gödel (1931)

Context

[…] a sufficiently explicit mathematical text could be expressed in a conventional language containing only a small number of fixed “words”, assembled according to a syntax consisting of a small number of unbreakable rules: such a text is said to be formalized. […] The verification of a formalized text is a more or less mechanical process […]. On the other hand, in an unformalized text, one is exposed to the dangers of faulty reasoning arising from, for example, incorrect use of intuition or argument by analogy. […] If, as happens again and again, doubts arise as to the correctness of the text under consideration, they concern ultimately the possibility of translating it unambiguously into such a formalized language. […] The axiomatic method is, strictly speaking, nothing but this art of drawing up texts whose formalization is straightforward in principle. — Nicolas Bourbaki (1939)

Definitions

Definition (Language)

Let \(\mathbb{A}\) be an alphabet \(\mathcal{F}\) a set of formation rules. A language is an ordered pair \(\mathcal{L}:=(\mathbb{A}, \mathcal{F})\).

Definition (Deductive Apparatus)

Let \(\mathcal{A}\) be a set of axiom schemas and \(\mathcal{I}\) the set of inference rules. A deductive apparatus is an ordered pair \(\mathcal{D}:=(\mathcal{A}, \mathcal{I})\).

Definition (Formal System)

Let \(\mathcal{L}\) be a language and \(\mathcal{D}\) a deductive apparatus. A formal system is an ordered pair \(\mathcal{S}:=(\mathcal{L}, \mathcal{D})\).

Concepts

Concept (Formalisation)

Let \(X\) be any declaration. Let \(\mathcal{S}\) be a formal system. A formalisation of \(X\) with respect to \(\mathcal{S}\) is the reduction of \(X\) in terms of \(\mathcal{S}\).

Concept (Machine-Assisted Formalisation)

Let \(X\) be any declaration. Let \(\mathcal{S}\) be a formal system. A machine-assisted formalisation of \(X\) with respect to \(\mathcal{S}\) is the reduction of \(X\) in terms of a computational implementation of \(\mathcal{S}\).

Why?

Motivation

Verifying

  • Checking results
  • Fixing mistakes
  • Filling gaps

Understanding

  • Gaining insight
  • Enhancing clarity
  • Facilitating generalisation
  • Empowering readers

Interacting

  • Working with instant feedback
  • Managing complexity

Collaborating

  • Enabling large-scale collaboration
  • Managing the literature
  • Teaching
  • Accelerating review process

Organising

  • Building digital libraries
  • Searching declarations
  • Refactoring libraries and proofs

Automating

  • AI for mathematics
  • Mathematics for AI

How?

Lean

  • Open source
  • General purpose
  • Functional programming language
  • Proof assistant
  • Dependent type theory

Lean Community

Mathlib

Differential Geometry in Mathlib

Planned

  • Riemannian metrics

In Review

  • Lie algebra of manifolds
  • Disjoint unions, products of manifolds
  • Inverse function theorem (for manifolds)
  • Orbifolds

In Progress

  • Local flows
  • Differential forms, de Rham cohomology
  • Oriented manifolds, orientations
  • Principal fibre bundles
  • API for the boundary of manifolds
  • (Unoriented) bordism groups
  • Sard’s theorem
  • API for local diffeomorphisms

Practice: Demo

Logistics

Workflow

  • Management
  • Design
  • Announcement
  • Coordination
  • Development
  • Review
  • Maintenance
  • Porting

Tools

Logistics: Projects

Future

Future

  • More differential geometry in Mathlib
  • LeanInformal (Demo 1, Demo 2)
  • Lean formalisation project space
  • More domain-specific automation
  • More integration with machine learning models
  • More integration with automated theorem provers
  • More integration with computer algebra systems

Proposal

Proposal

  • Expert consensus on feasibility 1
  • Community availability
  • What about a formal CHANGE?
  • Any project ideas?

Thanks!

Discussion