BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Vibe Formalisation and Slop Mathematics - Fenner Tanswell (Technis
 che Universität Berlin)
DTSTART:20260331T151500Z
DTEND:20260331T153000Z
UID:TALK245968@talks.cam.ac.uk
DESCRIPTION: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 t
 he use of vibe formalisation\, i.e. formalisation with an LLM but without 
 training or skill in using the formal language\, change research mathemati
 cs to make formal verification the norm rather than the exception? In this
  brief talk I will present a success case of vibe formalisation by&nbsp\;A
 lexeev and Mixon (2025)\,&nbsp\;and another case where it&nbsp\;is activel
 y unhelpful. The latter is the use of LLMs to vibe formalise crank mathema
 tics into Lean\, where the spaghetti code hides trivialising assumptions o
 r illicit definitions. I argue that this "slop mathematics" may be a serio
 us problem for the open science goals of research mathematics.&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR