Post #4136415
2026-07-27 11:57 UTC
@gallais@mamot.fr From the declaration:
"The increasing involvement of technology companies in mathematical research raises the risk that research questions may come to be prioritized because of their amenability to automated mathematics, rather than expert judgment of their deeper significance. "
Thus is already happening in my area. The people developing the tools discriminate on the type of proofs the tools support, while at the same time: demanding all papers to be mechanised; casting doubt on validity of mechanisation by tools other than their own."
Replies (1)
-
@markusde@mathstodon.xyz 2026-07-27 12:12
@ohad@mathstodon.xyz You know, I've been making two arguments that felt very different for some time now: - Verification systems can be made more effective by using a worse but more conventional probability theory, because there are fewer open problems you need to solve before using the tool. - The increasing expectations for papers to be formally verified will disadvantage interesting new ideas in favour of the status quo. It is now occurring to me, through your post, that the former quite is a compelling example for the latter. @gallais@mamot.fr