Post by @human_in_exile@mathstodon.xyz

2026-08-06 13:49 UTC

@tao@mathstodon.xyz But if its going to be made in NL for humans to understand anyway, like a journal, would people feel a need to formalise? At no stage really did someone say “my biggest issue with reading math journals is a computer didn’t mechanistically verify it in a language I do not understand” (or not many did if so, at least). There is never even a burden of understanding on the journal editors , they must usually assume you are wrong , and be convinced otherwise , in NL. As soon as they are confused they just stop reading and send it back, and if it was too "AI" you’d probably get black listed regardless of an attached theorem prover repo.

Replies (1)

@pandaninjas@infosec.exchange 2026-08-06 21:41

@human_in_exile@mathstodon.xyz @tao@mathstodon.xyz I feel there would still be a need to formalize, because it helps develop confidence in the fact that the solution is actually correct. For example, one theoretical computer science professor once described to me that their peer reviewer noted that one of the theorems in the paper was not adequately proven. They got this theorem from another paper, and went back and discovered a deficiency in the original proof of the theorem. Presumably, if there was a formalized certificate of the original proof, this issue could be avoided. Especially given that many AI proofs (right now) are the result of combining insights from a variety of distinct areas of math where one individual reviewer (or a team) would have difficulty understanding and digesting the entirety of the proof, formalization/verification could aid in assuring that the proof is correct.

Open ##5165742