Post #4232255

started my morning by reading this by Kevin Buzzard: https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/ On using GPT/Fable/etc to construct mathematics, then translate into systems like Lean. This is clearly working in some areas of maths, and that is huge. (I'm a AI skeptic. That someone well-respected is showing actual results over just pontificating is giving me pause for where this technology might actually be useful.)