News for hackers. Stuff that matters.

A comment on A recent experience with ChatGPT 5.5 Pro.

Re:A recent experience with ChatGPT 5.5 Pro by incrediblylarge on Saturday May 09, 2026 @02:03AM (#48072253)
A month ago my PhD supervisor told me it rips on proofs but he also said it's useless when formalising arguments in Lean - is this still the case?
[ Parent | on HN ]
Re:A recent experience with ChatGPT 5.5 Pro by vjerancrnjak on Saturday May 09, 2026 @02:09AM (#48072297)
Nope. Codex formalizes much better than any tool with exception of Aristotle from Harmonic.

https://github.com/vjeranc/fixed-rtrt

M3 module was formalized fully purely from experimental data and from a nudge by earlier versions of codex in 15-30 minutes in a simple write/compile/fix-first-error loop. I was a bit surprised how fast it picked up the pattern but given there was a paper from '70s it became clear why later.

[ Parent | on HN ]