[singularity2001]

They will have decades of experience with AI and they will be able to guide them by sniffing their hallucinations from single words.

[retrochameleon]

Hopefully in decades hallucinations will be largely solved.

[tempfile]

Hallucinations are an essential feature of the technology, they cannot be "solved". You may as well hope that we solve the halting problem.

[timacles]

its just as likely hallucinations will only get worse because their source data will be riddled with hallucinations

[eru]

You can't hallucinate a working lean proof.

[darkwater]

But you can hallucinate everything else.

[tempfile]

You absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?

[lanstin]

One of the concerns of the new LLM made lean proofs is ensuring they are using standard MathLib formulations in the theorem, so (quoting something in I longer recall the source of) a Grothendieck scheme is indeed what the reader and world know as a Grothendieck scheme.

[eru]

You read the stated theorem?