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 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
• Dylan McDermott, first postdoc, RU, now senior RA, U. of Oxford
• Joseph Tooby-Smith, postdoc, RU
• Dagur Ásgeirsson, PhD student, U. of Copenhagen
• Calvin Lee, PhD student, RU
• Yasuaki Morita, PhD student, RU
• Atli Franklín, PhD student, UI
• 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
• 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

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

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
• T. Uustalu and J. Tooby-Smith, 12-week BSc-level course Algebra and combinatorics, RU, Jan.-Apr. 2025
• A course on algebra and combinatorics, Agda used in practical sessions 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]

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

Schools and conferences hosted by us

• NLSS/SLS 2024, Reykjavik, June 2024
• FroCoS/ITP/TABLEAUX 2025, Reykjavik, Sept./Oct. 2025