BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//pretalx//pretalx.c3voc.de//qtcat-2026//speaker//TJTYGK
BEGIN:VTIMEZONE
TZID:CET
BEGIN:STANDARD
DTSTART:20001029T040000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20000326T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:pretalx-qtcat-2026-9F8KNH@pretalx.c3voc.de
DTSTART;TZID=CET:20260812T100000
DTEND;TZID=CET:20260812T110000
DESCRIPTION:Formalisation is the process of expressing mathematical ideas i
 n the\nlanguage understood by a proof assistant\, a computer program that\
 nenables the interactive construction of verified mathematical\ndefinition
 s\, theorems\, and proofs.\n\nThe stereotypical understanding of formalisa
 tion is as the rote\ntranslation of pre-existing mathematics to a cumberso
 me formal language\,\ndone primarily as a means of certifying the correctn
 ess of an argument.\nThis memetic conception as a chore standing in the wa
 y of a coveted\nresult (guaranteed correctness) has long allowed the aesth
 etics of\nformalisation to be appropriated by adversarial actors to furthe
 r their\nfinancial interests ("get paid for proving lemmas on the\nblockch
 ain"/"our new LLM will totally solve All Of Maths\, and we have\nthe Lean 
 to prove it").\n\nI aim to challenge this understanding\, presenting the p
 rocess of\nformalisation\, in itself\, as a force for good. I will share s
 ome of my\nown experiences with free-and-libre\, community-supported proof
 \nassistants as a tool for independent study\; genuine mathematical\ninsig
 hts revealed by developing category theory within formal univalent\ntype t
 heory\; and a few challenges that come with maintaining a library\nof form
 alised mathematics.
DTSTAMP:20260812T202113Z
LOCATION:R. 221
SUMMARY:Category theory\, formalised humanely - Amélia Liao
URL:https://pretalx.c3voc.de/qtcat-2026/talk/9F8KNH/
END:VEVENT
END:VCALENDAR