Icelandic advantage in computer-assisted proof (Iceproof)

Iceproof was a collaboration project (June 2024-May 2026) 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).

The goals were to 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 was the EU COST action EuroProofNet (2020-2025).

News

The 30th Nordic Congress of Mathematicians, NCM-30, to be held in Akureyri, 19-23 June 2027, will feature a special session on formalization of mathematics. Thierry Coquand is among the keynote speakers of the congress.

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, now lecturer, U. of Bath
• Dagur Ásgeirsson, initially PhD student, U. of Copenhagen, now 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, Tallinn UT → 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
• Tarmo Uustalu, Tallinn UT → Macquarie U., Sydney (to work with Richard Garner), 1-17 Nov. 2025 (paid by Macquarie U. and Tallinn U. of Techn.)
• Exequiel Rivas, London → RU, 30 Nov.-7 Dec. 2025
• Viviana del Barco, London → RU, 30 Nov.-7 Dec. 2025
• Matthieu Baty, UI → Rennes (POPL '27), 11-17 Jan. 2026
• Liisi Nõojärv, Tallinn UT → RU, 9-26 Feb. 2026
• Anders Claesson, UI → KTH, Stockholm, 15-19 March 2026
• Anders Claesson, UI → Boston (AMS Mtg.) + Northern Arizona U., Flagstaff, 26 March-8 April 2026
• Jacob Neumann, RU → Ljubljana (MFPS+SSTT '26), 30 May-6 June 2026

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 with J. Tooby-Smith, 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
• A. Claesson and M. Baty, 14-week BSc+MSc course Combinatorics, UI, Aug.-Nov. 2025
• An enumerative combinatorics course, Lean used for demonstration
• 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
• A. Claesson and M. Baty, 14-week BSc+MSc course Intro to logic, UI, Jan.-Apr. 2026
• A course in logic, Lean used for demonstration
• T. Uustalu and J. Neumann, 12-week BSc-level course Functional programming, RU, Jan.-Apr. 2026
• A course on programming in Haskell and Agda

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, Condensed mathematics in Mathlib, talk at seminar of Hausdorff Res. Inst. for Math. thematic trimester "Prospects of Formal Mathematics", Bonn, 13 June 2024 [video]
• 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
• T. Uustalu, The proof theory of skew logics (based on joint work with N. Veltri, C.-S. Wan, N. Zeilberger), talk at dept. seminar, U. di Verona, 23 October 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
• T. Uustalu, Sorting permutes: How to state and prove this in an intro course to computer-assisted proof?, presentation at IFIP WG 2.1 meeting #83, Viana do Castelo, 8-12 September 2025
• J. Tooby-Smith, PhysLean: digitalizing physics into Lean, talk at EuroProofNet Wksh. on Proof Libraries, Orsay, 15-16 Sept. 2025
• M. Baty, Building correct-by-construction hardware using proof assistants, talk at ICE-TCS seminar, RU, 26 September 2025
• J. Neumann, Dual-context directed type theory for synthetic-(co)inductive category theory, talk at Category Theory Octoberfest 2025, online, 25-26 October 2025
• T. Uustalu, Coherence for skew structures with proof theory (based on joint work with N. Veltri, C.-S. Wan, N. Zeilberger), talk at Australian Category Seminar, Macquarie U., Sydney, 5 November 2025
• A. Claesson, Counting fixed-point-free Cayley permutations (joint work with G. Cerbai), talk at Math. Colloquium, UI, 5 March 2026
• A. Claesson, Counting fixed-point-free Cayley permutations (joint work with G. Cerbai), talk at Combinatorics seminar, KTH, Stockholm, 18 March 2026
• A. Claesson, Counting fixed-point-free Cayley permutations (joint work with G. Cerbai), invited talk at AMS Spring Eastern Sectional Meeting, Boston, 28-29 March 2026
• A. Claesson, Counting fixed-point-free Cayley permutations (joint work with G. Cerbai), talk at Math. and Stat. Dept. Colloquium, Northern Arizona U., Flagstaff, 31 March 2026
• J. Neumann, nouGAT: calculating structures with Lean metaprogramming, talk at ICE-TCS seminar, RU, 17 April 2026
• J. Neumann, On auto-synthesis, talk at SSTT '26, Ljubljana, 4-5 June 2026

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
• V. del Barco, First integrals of the geodesic flow on nilpotent Lie groups, talk at Math. Colloquium, UI, 2 Dec. 2025
• E. Rivas, Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean (joint work with V. del Barco, G. Infanti, P. Schwahn), talk at ICE-TCS seminar, RU, 5 Dec. 2025

Schools and conferences hosted by us

• NLSS/SLS 2024, Reykjavik, 10-16 June 2024
• A summer school and a symposium on logic
• Lecturers of NLSS: Miika Hannula (U. of Helsinki), Sandra Kiefer (U. of Oxford), Greg Restall (U. of St. Andrews), Jandson Ribeiro (Cardiff U.), Rineke Verbrugge (U. of Groningen)
• Invited speakers of SLS: Fausto Barbero (U. of Helsink), Sara Negri (U. of Genova), Aybüke Özgün (U. of Amsterdam)
• 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 Titolo (Code Metal, ITP)