Re:Claude Fable produced a counterexample to the Jacobian Co...
by sciyoshi on Monday July 20, 2026 @12:48AM
(#48974470)
Looks like this has already been formalized: https://github.com/deancureton/jacobian
[ Parent
| on HN ]
Re:Claude Fable produced a counterexample to the Jacobian Co...
by bugufu8f83 on Monday July 20, 2026 @01:03AM
(#48974533)
To be clear, this is not the kind of thing where a Lean formalization provides any value at all. It's like formalizing the answer to a high school algebra problem. The counterexample is obviously correct.
Re:Claude Fable produced a counterexample to the Jacobian Co...
by sciyoshi on Monday July 20, 2026 @01:44AM
(#48974760)
Indeed. I was mainly responding to the comment about waiting for "independent seasoned mathematicians to verify", whereas in this case it is easy enough to convince oneself of the counterexample's correctness.