![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Fenner Tanswell (Technische Universität Berlin)
Tuesday 31 March 2026, 16:15-16:30
Vibe Formalisation and Slop Mathematics
- 👤 Speaker: Fenner Tanswell (Technische Universität Berlin)
- 📅 Date & Time: Tuesday 31 March 2026, 16:15 - 16:30
- 📍 Venue: Seminar Room 1, Newton Institute
Abstract
Most mathematicians don’t formalise their proofs because they don’t know how and don’t want to spend their time figuring it out. Might the use of vibe formalisation, i.e. formalisation with an LLM but without training or skill in using the formal language, change research mathematics to make formal verification the norm rather than the exception? In this brief talk I will present a success case of vibe formalisation by Alexeev and Mixon (2025), and another case where it is actively unhelpful. The latter is the use of LLMs to vibe formalise crank mathematics into Lean, where the spaghetti code hides trivialising assumptions or illicit definitions. I argue that this “slop mathematics” may be a serious problem for the open science goals of research mathematics.
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
Note: Ex-directory lists are not shown.