Icelandic advantage in computer-assisted proof (Iceproof)

Iceproof is a collaboration project (2024-2025) between Reykjavik University and the University of Iceland, funded by the Collaboration Fund of Iceland's Ministry of Higher Education, Science and Innovation (in March 2025 reorganized into the Ministry of Culture, Innovation and Higher Education).

In Iceproof, we introduce the technology of computer-assisted proof into teaching of computer science and mathematics at RU and UI, bring it to IT professionals in Iceland, boost Icelandic research in the field and increase its visibility.

A project on the European level with overlapping aims is the EU COST action EuroProofNet (2020-2025).

People

Contributors

• Tarmo Uustalu, professor, RU, project leader
• Anders Claesson, professor, UI, project leader at UI
• Matthieu Baty, postdoc, UI
• Dylan McDermott, initially postdoc, RU, now senior RA, U. of Oxford
• Jacob Neumann, postdoc, RU
• Joseph Tooby-Smith, postdoc, RU, soon lecturer, U. of Bath
• Dagur Ásgeirsson, initially PhD student, U. of Copenhagen, soon postdoc, U. of Alberta, Edmonton
• Atli Franklín, PhD student, UI
• Calvin Lee, PhD student, RU
• Yasuaki Morita, PhD student, RU
• Bjarki Gunnarsson, MSc student, UI

Collaborators

• Thorsten Altenkirch, U. of Nottingham
• Peter Dybjer, Chalmers U. of Technology

Activity

Research and conference visits

• Nathanael Arkor, Tallinn UT → RU, 9-17 March 2024 (funded by EuroProofNet)
• Philip Saville, U. of Oxford → RU, 9-18 March 2024 (funded by EuroProofNet)
• Dylan McDermott, RU → U. of Cambridge (to work with Martin Hyland), 11-18 Aug. 2024 (funded by EuroProofNet)
• Giulio Fellin, U. of Brescia → RU, 30 Aug.-8 Sept. 2024
• Christian Bean, Keele U. → UI, 1-6 Sept. 2024
• Thorsten Altenkirch, U. of Nottingham → RU, 1-7 Sept. 2024 (funded by EuroProofNet)
• Tarmo Uustalu, RU → U. of Verona, 19 Oct.-1 Nov. 2024 (paid by U. of Verona)
• Philipp Joram, Tallinn UT → RU, 22 Nov.-5 Dec. 2024
• Niccolò Veltri, Tallinn UT → RU, 18-23 Feb. 2025 (paid by Tallinn UT)
• Pierre-Louis Curien, IRIF, U. Paris Cité → RU, 12-30 March 2025
• Jacob Neumann, U. of Nottingham → RU, 21-30 April 2025
• Luís Pinto, U. of Minho → RU, 22 Apr.-1 May 2025
• Jacob Neumann, Reykjavik → Glasgow (TYPES '25), 7-15 June 2025
• Dagur Ásgeirsson, Akureyri → Vienna (LC '25), 8-10 July 2025

Project internal meetings

• Meeting in Bifröst, 3-5 Sept. 2024, with Thorsten Altenkirch (U. of Nottingham), Christian Bean (Keele U.) and Giulio Fellin (U. of Brescia) as guests
• Meeting in Reykholt in Borgarfjörður, 23-25 Apr. 2025, with Jacob Neumann (U. of Nottingham) and Luís Pinto (U. of Minho) as guests

Results

Courses by us

• T. Uustalu, short (12 h) MSc-level course Substructural logics à la Lambek, U. of Verona, 19-31 Oct. 2024
• T. Uustalu, 3-week intensive MSc-level course Introduction to computer-assisted proof, RU, Nov.-Dec. 2024
• An intro to certified programming using Agda
• A. Claesson, short (4×60 min) course Combinatorial species, EWSCS '25, Viinistu, 3-6 March 2025
• T. Uustalu, 3-week intensive MSc-level course Programming language semantics with applications, RU, Nov.-Dec. 2025
• A course on programming language semantics, Agda used for demonstration

Talks by us

• D. Ásgeirsson, Condensed mathematics in Mathlib, talk at Lean Together 2024, online, 9-12 Jan. 2024 [video]
• D. Ásgeirsson, Lean and its mathematical library, talk at ICE-TCS seminar, RU, 15 Feb. 2024
• T. Uustalu, Skew categorical logic (based on joint work with N. Veltri, C.-S. Wan, N. Zeilberger), talk at Math. Colloquium, UI, 14 March 2024
• D. Ásgeirsson, Towards solid abelian groups: a formal proof of Nöbeling's theorem, talk at ITP 2024, Tbilisi, 9-14 Sept. 2024
• J. Tooby-Smith, Lean and the physical sciences, talk at ICE-TCS seminar, RU, 2 Oct. 2024
• J. Tooby-Smith, Lean and physics, talk at Lean Together 2025, online, 14-17 Jan. 2025 [video]
• J. Tooby-Smith, Introduction to PhysLean, discussion with G. Carcassi (U. of Michigan) in the podcast of the Assumptions of Physics project, online, 8 March 2025 [video]
• J. Tooby-Smith, Interactive theorem provers and mathematics, talk at Math. Colloquium, UI, 15 May 2025
• J. Neumann, Synthetic-inductive category theory, talk at TYPES '25, Glasgow, 9-13 June 2025
• D. Ásgeirsson, Formalized condensed mathematics, special session invited talk at Logic Colloquium '25, Vienna, 7-11 July 2025
• J. Tooby-Smith, PhysLean: digitalizing physics into Lean, talk to the Complex Quantum Systems Group, U. of Maryland, online, 8 July 2025

Talks by guests

• T. Altenkirch, Πthon - dependently typed Python (joint work with A. Penzes), talk at ICE-TCS seminar, RU, 6 Sept. 2024
• P. Joram, Data types with symmetries via action containers (joint work with N. Veltri), talk at ICE-TCS seminar, RU, 29 Nov. 2024
• N. Veltri, Semi-associative substructural logics (joint work with C.-S. Wan), talk at ICE-TCS seminar, RU, 21 Feb. 2025
• P.-L. Curien, Clones as monoids (joint work with A. Bucciarelli, A. Salibra), talk at ICE-TCS seminar, RU, 14 March 2025
• P.-L. Curien, Facets of coherence (joint work with G. Laplante-Anfossi), talk at Math. Colloquium, UI, 20 March 2025

Schools and conferences hosted by us

• NLSS/SLS 2024, Reykjavik, June 2024
• FroCoS/ITP/TABLEAUX 2025, Reykjavik, 27 Sept.-2 Oct. 2025
• Three conferences on theorem proving + workshops on Rocq and Lean
• Invited speakers: Kaustuv Chaudhuri (LIX, Inria/École Polytechnique, FroCoS+TABLEAUX), Carsten Fuhs (Birkbeck, University of London, FroCoS), Raheleh Jalali (U. of Bath, TABLEAUX), Kathrin Stark (Heriot Watt U., ITP), Laura Titulo (Code Metal, ITP)