Faculty of Science

Formalisation of Mathematics (masterclass)
Provider: Faculty of Science

Activity no.: 5555-23-07-31
	Enrollment deadline: 21/06/2023

Place

Department of Mathematical Sciences

Date and time

26.06.2023, at: 09:00 - 30.06.2023, at: 16:00

Regular seats

ECTS credits

2.50

Contact person

Nina Weisse E-mail address: weisse@math.ku.dk

Enrolment Handling/Course Organiser

Dustin Clausen E-mail address: dustin.clausen@math.ku.dk

Written language

English

Teaching language

English

Course workload

Course workload category	Hours
Preparation / Self-Study	30.00
Course hours	40.00
Evaluation / reporting	5.00

Sum	75.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)

Click the search button to search Courses.

See which courses you can attend and when

Jan	Feb	Mar	Apr
May	Jun	Jul	Aug
Sep	Oct	Nov	Dec