(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
PROGRAMME (NEW: including abstracts, slides and full videos) :
9h30 – 10h : Andrei Rodin (SPHERE, Paris-Cité):
A Long History of Formalisation and Deformalisation in Mathematics (abstract)(slides)(video)
10h-10h45 : Thierry Coquand (University of Gothenburg)
Dependent type theory and formalisation of mathematics (abstract)(slides)(video)
10h45-11h : COFFEE BREAK
11h-11h45 : Sergei Artemov (City University of New York)
Non-Compact Proofs (abstract)(slides)(video)
11h45 – 12h30 : Elijah Gadsby (City University of New York)
Selector Proofs and Hierarchies of Logical Strength (abstract)(slides)(video)
12h30 – 14h : LUNCH
14h-14h45 : Daniel Rogozin (Noeon Research)
Operational Knowledge Representation with Monoidal Categories and Linear Type Theory )(abstract) (slides)(video)
14h45-15h30 Sophie d’Espalungue (IRIF, Paris-Cité)
Foundational Aspects of Size and Dimension in Higher Categorical Structures (abstract)(slides)(video1:slides)(video2:whiteboard)
15h30 – 15h45 COFFEE BREAK
15h45-16h30 Paul-André Melliès (IRIF, Paris-Cité)
A la Recherche du Flux Logique et Linguistique (abstract)(slides)(video)
16h30-18h Round Table (video)