Or maybe the AI didn’t write Lean proof at all, or rather, not the LLM at least. But instead OpenAI has an internal traditional reinforcement model that is able to stumble on the Lean proof by the share amount of compute power available to them thousand monkeys on a thousand typewriter style. And then pretend LLM did it because that is what they are selling.

▲

nbulka 30 minutes ago | parent | next [-]

Not necessarily monkeys but thinking in Lean first is quite plausible

▲

famouswaffles 5 hours ago | parent | prev [-]

[flagged]

▲

runarberg 5 hours ago | parent [-]

I don’t. But I do know how the scientific method works, and OpenAI’s display is anything but. Until what they have demonstrated is reproduced I take their claims to be nothing but marketing. A for profit company will lie in order to maximize their profits. Above I presented an alternative hypothesis, which is probably wrong, but until OpenAI’s results are replicated I will believe my alternative hypothesis just as much as I believes the claims of the for profit company making them.

▲

phoghed 4 hours ago | parent [-]

I’m a non-math layman, and not a scientific method knower like yourself. How does one usually “replicate” a math or Lean proof?

	▲	krupan 38 minutes ago \| parent \| next [-]
		It's the method they used to create the proof that's in question here. They claim their amazing product did it, and therefore you should buy their product because will do amazing things for you too!
	▲	bordercases 4 hours ago \| parent \| prev \| next [-]
		Hopefully not in the same way you should never naively trust compilers!
	▲	runarberg 3 hours ago \| parent \| prev [-]
		The generation of the proof can be replicated. And if it can‘t we should be suspicious of their claims.