Gemini about FRO plans for Lean 4.20

Stream: general

[Yury G. Kudryashov]

Here is what Gemini says if you search for "Lean 4.20" in Google:

Lean v4.20 is a complete verifier for Lean 4, which is a theorem prover and programming language. It is the first verifier for Lean 4 that is not the reference implementation in C++. The new verifier is able to verify all of Lean's mathlib library and runs 20–50% slower than the original.

The second sentence goes with a link to @Mario Carneiro 's paper on Lean4Lean (found by @Cameron Zwarich).

[Edward van de Meent]

just to be clear, is this accurate?

[Henrik Böving]

Complete hallucination

[Edward van de Meent]

ah

[Edward van de Meent]

is it a bad idea tho? :upside_down:

[Mario Carneiro]

I think it's more or less accurate if you find/replace Lean 4.20 with Lean4Lean

[Henrik Böving]

Yes

[Shreyas Srinivas]

How apt that an AI should hallucinate on 4.20. In some parts of India "420" is synonymous with fraud, because that's the section of the law dealing with it.

[Mario Carneiro]

In the US I guess you could also say that 4.20 is associated with hallucination

[Edward van de Meent]

i mean, if i were to ask it a question like "at what version of lean is [bla bla bla]", i do think that an answer involving the numerals 4 and 2 in that order (preferably with none inbetween) is better than another number...

[Edward van de Meent]

there is something about four-two that has a question-answering quality about it...