Verification time is the price nobody quotes
AI output is priced per token, but you pay for it in the minutes it takes a person to check it. Any productivity claim that leaves out checking time is measuring the wrong thing.
Blog / Category
Systems
Posts filed under Systems.
What "verified in Lean" does and doesn't buy you
A Lean proof guarantees the proof follows from the statement. It says nothing about whether the statement is the one you care about. AI-generated proofs make that gap the main event.