Post #1491892
2026-04-11 22:02 UTC
working on writing a blog post which i've been calling "structure and interpretation of mathematical theories." i was originally planning to write something fairly narrow, talking about typeclasses and locales, and how they can be used to structure mathematical theories within a proof assistant, but the more that i write, the more my thoughts are diverging into something much broader
Replies (1)
-
@mra@mathstodon.xyz 2026-04-11 22:10
one thing that's been on my mind is the role of proof assistants. @johncarlosbaez started a great thread a week or so ago about the role of formalisation in mathematics. martin escardo said something in that thread that stuck with me, basically talking about using proof assistants as a tool of thought. like any tool of thought, i think that it's important to understand that any proof assistant will necessarily have limits to its expressive capabilities, or design decisions which demand that thought be laid out in a certain way, and that mathematical thought does not have to fit within the box of the expressive capabilities of any proof assistant to be valid, worthwhile mathematical thought