@thinkb4coding@mastodon.social
2026-09-11 23:56 UTC
@tao@mathstodon.xyz if I understand correctly the situation, IA companies just brute force problems with solvers as rocq injecting far more money than research ever had to produce slop proofs (valid proof that are still meaningless).
Replies (1)
-
@thinkb4coding@mastodon.social 2026-09-11 23:57
@tao@mathstodon.xyz this is in no way a sustainable way to do maths, and it's harmful.