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
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 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
- 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, 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,
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)
Last update 29 August 2025