{"guid":"030bbd5a-36ca-58c3-847f-5c42016f0f27","title":"Category theory, formalised humanely","subtitle":null,"slug":"qtcat-2026-110771-category-theory-formalised-humanely","link":"https://pretalx.c3voc.de/qtcat-2026/talk/9F8KNH/","description":"Formalisation is the process of expressing mathematical ideas in the\nlanguage understood by a proof assistant, a computer program that\nenables the interactive construction of verified mathematical\ndefinitions, theorems, and proofs.\n\nThe stereotypical understanding of formalisation is as the rote\ntranslation of pre-existing mathematics to a cumbersome formal language,\ndone primarily as a means of certifying the correctness of an argument.\nThis memetic conception as a chore standing in the way of a coveted\nresult (guaranteed correctness) has long allowed the aesthetics of\nformalisation to be appropriated by adversarial actors to further their\nfinancial interests (\"get paid for proving lemmas on the\nblockchain\"/\"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 process of\nformalisation, in itself, as a force for good. I will share some of my\nown experiences with free-and-libre, community-supported proof\nassistants as a tool for independent study; genuine mathematical\ninsights revealed by developing category theory within formal univalent\ntype theory; and a few challenges that come with maintaining a library\nof formalised mathematics.\n\nLicensed to the public under https://creativecommons.org/licenses/by/4.0/","original_language":"eng","persons":["Amélia Liao"],"view_count":890,"promoted":false,"date":"2026-08-12T10:00:00.000+02:00","release_date":"2026-08-12T00:00:00.000+02:00","updated_at":"2026-08-21T20:45:09.613+02:00","tags":["9F8KNH","2026","qtcat2026","R. 221","qtcat2026-eng","Day 1"],"length":3842,"duration":3842,"thumb_url":"https://static.media.ccc.de/media/events/qtcat/2026/110771-030bbd5a-36ca-58c3-847f-5c42016f0f27.jpg","poster_url":"https://static.media.ccc.de/media/events/qtcat/2026/110771-030bbd5a-36ca-58c3-847f-5c42016f0f27_preview.jpg","timeline_url":"https://static.media.ccc.de/media/events/qtcat/2026/110771-030bbd5a-36ca-58c3-847f-5c42016f0f27.timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/events/qtcat/2026/110771-030bbd5a-36ca-58c3-847f-5c42016f0f27.thumbnails.vtt","frontend_link":"https://media.ccc.de/v/qtcat-2026-110771-category-theory-formalised-humanely","url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_title":"Queer and Trans People in Category Theory 2026","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026","related":[],"recordings":[{"length":3841,"mime_type":"video/mp4","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2026-08-12T16:56:35.016+02:00","label":"eng 1080p","size":264,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/h264-hd/qtcat2026-110771-eng-Category_theory_formalised_humanely_hd.mp4","url":"https://api.media.ccc.de/public/recordings/103269","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3842,"mime_type":"audio/opus","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_opus.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2026-08-12T16:59:13.556+02:00","label":"eng","size":36,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/opus/qtcat2026-110771-eng-Category_theory_formalised_humanely_opus.opus","url":"https://api.media.ccc.de/public/recordings/103271","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3842,"mime_type":"audio/mpeg","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_mp3.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2026-08-12T16:59:18.009+02:00","label":"eng","size":59,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/mp3/qtcat2026-110771-eng-Category_theory_formalised_humanely_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/103272","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3841,"mime_type":"video/mp4","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2026-08-12T17:01:33.415+02:00","label":"eng 576p","size":110,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/h264-sd/qtcat2026-110771-eng-Category_theory_formalised_humanely_sd.mp4","url":"https://api.media.ccc.de/public/recordings/103274","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3842,"mime_type":"video/webm;codecs=av01","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_av1-hd.webm","state":"new","folder":"av1-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2026-08-12T17:12:35.389+02:00","label":"eng 1080p","size":208,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/av1-hd/qtcat2026-110771-eng-Category_theory_formalised_humanely_av1-hd.webm","url":"https://api.media.ccc.de/public/recordings/103281","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3842,"mime_type":"video/webm","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2026-08-12T17:32:36.990+02:00","label":"eng 1080p","size":286,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/webm-hd/qtcat2026-110771-eng-Category_theory_formalised_humanely_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/103285","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"},{"length":3842,"mime_type":"video/webm","language":"eng","filename":"qtcat2026-110771-eng-Category_theory_formalised_humanely_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2026-08-12T17:49:33.676+02:00","label":"eng 576p","size":127,"recording_url":"https://cdn.media.ccc.de/events/qtcat/2026/webm-sd/qtcat2026-110771-eng-Category_theory_formalised_humanely_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/103291","event_url":"https://api.media.ccc.de/public/events/030bbd5a-36ca-58c3-847f-5c42016f0f27","conference_url":"https://api.media.ccc.de/public/conferences/qtcat2026"}]}