Post #3963399

Replies (1)

• @ask@infosec.exchange 2026-07-20 16:05

  In fact when I graduated I had kind of a hard time realizing that you can't really do math alone. Math has this air of perfect logic independent of even the universe and yet without a community of human mathematicians to check your work and agree with your logic and learn together it doesn't really mean anything and there's no way of knowing if you're correct or subtly wrong. When I had this thought it was about how when you write a proof it's not in full detail and humans have to fill in the blanks as they read to see if they agree with the proof. So the situation changes somewhat when you involve mechanical proof checkers. However I think it's ultimately the same thing again at a different level. It's critical to write the theorem statement exactly correctly and subtle variations can make the proof uninteresting and not what the community wanted to learn. So you can't really write a theorem statement to work on a proof for without contact with the community. Even the existence of the proof checker program is predicated on the human community that built it and decided that it correctly represents the logic they care about.

  Open ##3963822