Post #2134789
2026-04-11 22:10 UTC
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
Replies (1)
-
@mra@mathstodon.xyz 2026-04-11 22:16
for instance, ink on paper has been the primary tool for the expression of mathematical thought for a very long time, but this tends to impose a kind of linearity to the expression of thought. think of all of the textbooks which begin with a kind of "dependency graph," showing which chapters of the book depend on the contents of which other chapters. this is a kind of kludge to get around the limitations of the tool of thought being used! there are projects, like amélia liao's venerable 1lab, which use hypertext instead of ink on paper! hypertext gets around this particular limitation of paper as a tool of thought, but of course it has its own limitations!