AI is moving into verifiable, high-stakes work
Two stories show AI aimed at problems with a hard right answer. The classification of finite simple groups is now formalized in Lean, at 43.1M lines. A commenter notes this is a good fit for auto-formalization because mathematicians have previously believed the classification was finished, only to find a missing class. Another asks whether you can point a frontier model at every math textbook and convert it all to Lean. Anthropic also posted early progress on speeding up drug development with Claude, and Google DeepMind released Genie 4.
The reaction to the drug post is the interesting part. A commenter with a rare disease says they'd love to see it help but is cautious, because "murine models still take time, and clinical trials are slow." Another notes the page has a big chapter picker with only two chapters.
The pattern: AI wins first where an output can be checked by a proof assistant, a test, or a compiler. It wins more slowly where the bottleneck is the physical world.
So what?
Build AI products where output can be verified automatically, because that is where trust and revenue come fastest. Where your bottleneck is wet labs, trials, or regulators, expect AI to shave the cheap part of the timeline, not the slow part.