(in the context of automated theorem proving and beyond)
One-day workshop organised as a part of regular seminar on History and Philosophy of Mathematics in laboratory SPHERE, University Paris-Cité, on February 23, 2026 from 9h30 to 18h CET (the time zone of Paris) (FLYER)
Description:
Recent developments in foundations of mathematics and automated theorem proving significantly changed the received view on formalisation forged during the foundational debates of the first half of the 20th century and their historical and philosophical codification during the second half of this century. The new 21st century brought the project of univalent foundation (since 2006) and a booming (and partly unrelated) development in the automated theorem proving. The following questions are today largely open, and we propose to discuss them during the workshop (journée d’études):
– is a universal formalisation desirable or multiple formalisations of the same contents should be admitted?
– what are the roles of natural languages and formal calculi in the traditional and
computer-assisted mathematics?
– (de)formalisation in the context of automated theorem proving;
– which formal calculi are appropriate for formalising mathematics?
– formalisation and logical foundations; can a formalisation of mathematics be foundation-free?
– « blind computation» and contentual reasoning in mathematics and logic
– the « old » and the « new » conceptions of formalisation of mathematics: making the ends meet.
When: February 23, 2026 from 9h30 to 18h.
Where: Paris, SPHERE (University Paris-Cité, Room 628 at the Olympe de Gouges building, Place Paul Ricoeur 75013 Paris) and INTERNET
SCHEDULE :
9h30 – 10h : Andrei Rodin (SPHERE, Paris-Cité):
A Long History of Formalisation and Deformalisation in Mathematics (introductory remarks)
10h-10h45 : Thierry Coquand (University of Gothenburg)
Dependent type theory and formalisation of mathematics
10h45-11h : COFFEE BREAK
11h-11h45 : Sergei Artemov (City University of New York)
Non-Compact Proofs
11h45 – 12h30 : Elijah Gadsby (City University of New York)
Selector Proofs and Hierarchies of Logical Strength
12h30 – 14h : LUNCH
14h-14h45 : Daniel Rogozin (Noeon Research)
Operational Knowledge Representation with Monoidal Categories and Linear Type Theory
14h45-15h30 Sophie d’Espalungue (IRIF, Paris-Cité)
Foundational Aspects of Size and Dimension in Higher Categorical Structures
15h30 – 15h45 COFFEE BREAK
15h45-16h30 Paul-André Melliès (IRIF, Paris-Cité)
A la Recherche du Flux Logique et Linguistique
16h30-18h Round Table
Titles and Abstracts (in the alphabetical order of speakers’s names):
Sergei Artemov (City University of New York)
Title: Non-Compact Proofs
Abstract:
Non-compact proofs are used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on arithmetical proofs of universal statements (*) “for any natural number n, F(n).” A proof of (*) is compact if all proofs of F(n)’s for n=0,1,2,… fit into some finitely axiomatized fragment of Peano Arithmetic PA. An example of non-compact reasoning is the standard proof of Mostowski’s 1952 reflexivity theorem: PA proves the consistency of its finite fragments.
It turns out that Gödel’s Second Incompleteness Theorem, G2, prohibits compact proofs but does not rule out non-compact proofs of PA-consistency formalizable in PA. This explains why and how the recent proofs of PA-consistency in PA work: they essentially formalize in PA the explicit version of Mostowski’s non-compact proof and use Gödelian provable explicit reflection to rid redundant provability operators.
These findings yield a new foundational reading of G2: “the consistency of PA is not provable within a finite fragment of PA,” complemented with the positive message: “the consistency of PA is provable within the whole PA.” This perspective suggests that Gödel’s theorem does not represent a failure of the system to “know” its own consistency, but rather a structural limit on how that knowledge can be packaged into a single finite string.
Thierry Coquand (University of Gothenburg)
Title: Dependent type theory and formalisation of mathematics
Abstract:
I will to give arguments, both using history of type theory and actual mathematical examples,
why dependent type theory with the axiom of univalence is well-suited for a formal representation of mathematical concepts and proofs.
Sophie d’Espalungue (Paris-Cité)
Title: Foundational Aspects of Size and Dimension in Higher Categorical Structures
Abstract:
This talk investigates the structure and role of universes in the formalisation of higher categorical structures, towards a formalisation of the hierarchy of the (very large) n+1-category of n-categories. The focus is on motivations and conceptual aspects of ongoing work. I will review notions of smallness in higher categorical structures, bringing together perspectives from homotopy type theory and more classical categorical intuitions. I will then discuss how truncation hierarchies — such as n-truncated types and n-categories — interact with universes under univalence, and use it to outline connections between HoTT and the framework I am developing.
Elijah Gadsby (City University of New York)
Title: Selector Proofs and Hierarchies of Logical Strength
Abstract:
Under the standard formalisation paradigm, it has been known since Gödel that there is no complete theory of mathematics. There is instead a hierarchy of theories that can be organised by different measures of logical strength (which coincide in natural cases). Artemov has introduced the notion of a selector proof as the logical framework for a type of reasoning common in mathematical practice but omitted in the traditional account. We shall reexamine these logical hierarchies in the presence of selector proofs, where a theory can selector prove its own consistency. Technical results concerning selector proofs, their limitations, and their relationships to traditional formal proofs will be presented, and it will be seen that key aspects of the traditional picture reappear in a new guise. We take this to be evidence of the robustness of the ideas underlying these notions of logical strength.
Paul-André Melliès (CNRS, Université Paris Cité, INRIA)
Title: A la recherche du flux logique et linguistique
Abstract :
Dans cet exposé, j’aborderai la question de comprendre comment nous accédons comme lecteurs et lectrices à la compréhension logique et linguistique d’un texte mathématique. Je discuterai en particulier de points de rapprochement inattendus et prometteurs entre interprétation interactive du raisonnement logique, et analyse syntaxique (ou parsing) de la phrase dans les grammaires catégorielles. J’expliquerai dans le même mouvement comment l’exécution par beta-réduction du lambda-calcul peut être comprise comme une forme d’exploration interactive entre stratégies et contre-stratégies de preuves ; et comment cette exécution se dessine au moyen de diagrammes de cordes inspirés de la physique, où le flux logique et linguistique circule à la manière d’une particule dans le texte de la démonstration.
Mon exposé repose sur les chapitres 4, 6 et 7 de mon habilitation Une étude micrologique de la négation (HDR Université Paris Cité, novembre 2017 https://www.irif.fr/~mellies/habilitation.html), sur mon travail avec Noam Zeilberger sur les grammaires hors contextes
The categorical contours of the Chomsky-Schützenberger representation theorem.
(Logical Methods in Computer Science, Volume 21, Issue 2, May 16, 2025,
https://arxiv.org/abs/2405.14703), ainsi que sur des discussions récentes avec Philippe de Groote, dans le cadre du projet Malinca.
Andrei Rodin (SPHERE, Paris-Cité)
Title: A Long History of Formalisation and Deformalisation in Mathematics
Abstract: Using formal symbolic means in mathematics historically predates reliance on natural language to support informal mathematical reasoning. The interplay between these two aspects of mathematics has been a key factor in the discipline’s development throughout its history, and it remains so today in the new context of automated theorem proving.
Daniel Rogozin (Noeon Research)
Title: Operational Knowledge Representation with Monoidal Categories and Linear Type Theory
Abstract:
The current mainstream direction in modelling reasoning and knowledge is becoming, in the speaker’s opinion, over-focused on the solutions based on the large language models and machine learning. In this talk, we discuss how one can provide the mathematical rationale for the concept of operational knowledge, that is, a sort of knowledge understood as an ability to solve this or that task by performing a required action. We argue that an appropriate mathematical modelling of operational knowledge is not sufficient if we just think of it in terms of statistical approximations, but also must include a developed framework of how we represent ontology by mathematical means to achieve higher levels of interpretability without oversimplifying the epistemological aspects. We suggest that we make this objective closer by developing knowledge representation as a separate theoretical discipline with the mathematical foundations based on monoidal categories and linear type theory.