Login for PhD students/staff at UCPH      Login for others
Formalisation of Mathematics (masterclass)
Provider: Faculty of Science

Activity no.: 5555-23-07-31 
Enrollment deadline: 21/06/2023
PlaceDepartment of Mathematical Sciences
Universitetsparken 5, 2100 København Ø
Date and time26.06.2023, at: 09:00 - 30.06.2023, at: 16:00
Regular seats60
ECTS credits2.50
Contact personNina Weisse    E-mail address: weisse@math.ku.dk
Enrolment Handling/Course OrganiserDustin Clausen    E-mail address: dustin.clausen@math.ku.dk
Written languageEnglish
Teaching languageEnglish
Course workload
Course workload categoryHours
Preparation / Self-Study30.00
Course hours40.00
Evaluation / reporting5.00
Sum75.00
Content
The masterclass will present recent advances in the formalisation of mathematics using the programming language Lean.

In recent years there has been a strong push towards formalising mathematics using so called proof assistants. This means that mathematical theory is written in a programming language allowing the software to formally verify its correctness. In doing so, it allows to construct a database of all mathematical knowledge and enables researchers to collaborate on a whole new scale resembling the ways of modern software development. The goal of the masterclass is to teach participants the skills necessary to participate in such projects.

The invited speakers, Adam Topaz and Kevin Buzzard, were two of the main contributors in an extremely successful recent project, called the Liquid Tensor Experiment, which formalised a hard theorem in the new field of condensed mathematics. The focus of the masterclass will be to present this project and recent developments. There will be an emphasis on exercises and having participants work on projects themselves using the Lean Theorem Prover.

Proof assistants such as the Lean Theorem Prover are revolutionising how mathematicians work. They facilitate larger collaborations than what was previously possible in mathematics, because the computer can keep track of the big picture while individual collaborators can focus entirely on smaller parts of the puzzle. This masterclass will teach mathematicians how to effectively incorporate this new technology in their research, creating a stepping stone into the future of mathematics.

Remarks
Visit the masterclass website: https://www.math.ku.dk/english/calendar/events/formalisation-of-mathematics/

Contact: Dagur Tomas Asgeirsson (dagur@math.ku.dk), Boris Bolvig Kjær (bbk@math.ku.dk)

Search
Click the search button to search Courses.


Course calendar
See which courses you can attend and when
JanFebMarApr
MayJunJulAug
SepOctNovDec



Publication of new courses
All planned PhD courses at the PhD School are visible in the course catalogue. Courses are published regularly.