> Autoformalization has become a practical reality in 2026

Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.

▲

gus_massa 3 hours ago | parent | next [-]

> prove something different

I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?

	▲	Retric 2 hours ago \| parent [-]
		No, prove something else could mean proving something very trivial thus making the proof meaningless on its own. IE a proof can be true, rigorous, and not at all what was asked for.

▲

tomkeen 3 minutes ago | parent | prev | next [-]

[flagged]

▲

an hour ago | parent | prev [-]

[deleted]