5 ms·

I wouldn't be surprised if half these proofs turn out to be well crafted hallucinations, barring of course the ones actually verified in Lean

• evenhash 1mo ago
  Being “verified in Lean” doesn’t magically solve the problem of hallucinations unfortunately. It just shifts the work from > reading the (natural language) proof and confirming it has no errors to > reading the Lean code and confirming it correctly encodes the theorem For example here is a statement of the Pythagorean theorem in Lean: theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ <-> angle p₁ p₂ p₃ = Real.pi / 2 This is just one possible way of formalizing it and it depends on other definitions, wherein you also need to understand the assumptions they make, etc. Answering the question of “whether proving this theorem in Lean proves the Pythagorean theorem” thus requires expert judgement as well as domain knowledge of Lean’s libraries. So if the AI says “this theorem is true, here is the proof in Lean” it’s still possible that it’s not correct, even if the Lean code compiles. The result will still be in question until a human expert reviews it.