Make lean proofs more readable?

Stream: general

[fzyzcjy]

Hi, when learning Isabelle, I feel that (as really non-expert in proof assistants) the cantor's theorem is a bit more readable in Isabelle than Lean mathlib. In other words, the Isabelle proof resembles more the proofs in human language. Thus, I wonder:

1. Is it a fundamental limit of Lean that Lean proofs are not that human readable? (I guess we can use have keyword in Lean, but I am not sure why it is not that frequently used; In addition, it seems Lean's automation is not that powerful)
2. Is it / will it be a priority in Lean to make proofs human readable? (Or it is favored to write down hard-to-read but easy-to-write proofs to speed up proving)
   P.S. I like Lean's ecosystem, community, etc, and hope I can use it!

Lean:

/-- **Cantor's theorem** -/
theorem cantor (a : Cardinal.{u}) : a < (2^a) := by
  induction' a using Cardinal.inductionOn with α
  rw [← mk_set]
  refine' ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, _⟩
  rintro ⟨⟨f, hf⟩⟩
  exact cantor_injective f hf
#align cardinal.cantor Cardinal.cantor

/-- **Cantor's diagonal argument** implies that there are no injective functions from `Set α`
to `α`. -/
theorem cantor_injective {α : Type*} (f : Set α → α) : ¬Injective f
  | i => cantor_surjective (fun a ↦ {b | ∀ U, a = f U → U b}) <|
         RightInverse.surjective (λ U => Set.ext <| fun _ ↦ ⟨fun h ↦ h U rfl, fun h _ e ↦ i e ▸ h⟩)

theorem cantor_surjective {α} (f : α → Set α) : ¬Surjective f
  | h => let ⟨D, e⟩ := h {a | ¬ f a a}
        @iff_not_self (D ∈ f D) <| iff_of_eq <| congr_arg (D ∈ ·) e

while Isabelle:
image.png

[Mario Carneiro]

The proof is pretty golfed. You can of course write a version of the proof similar to the isabelle proof

[Mario Carneiro]

theorem cantor_surjective {α} (f : α → Set α) : ¬Surjective f := by
  intro (h_surj : Surjective f)
  have : ∀ A, ∃ a, f a = A := h_surj
  obtain ⟨a, e : f a = {x | x ∉ f x}⟩ := this _
  have : a ∈ f a ↔ a ∈ {x | x ∉ f x} := by rw [e]
  show False; exact iff_not_self this

[Mario Carneiro]

Of course we don't have tactics like blast; improving in this regard is a long standing issue

[fzyzcjy]

@Mario Carneiro Thank you, that one does look readable for me!
So I wonder, whether Lean community will tend to make proofs human readable?
My area is about ML/AI for theorem proving. If a proof is easier to understand by humans (e.g. the lean proof you provided), I guess it may be easier for AI to learn from it.

[Mario Carneiro]

People write proofs according to their tastes

[fzyzcjy]

I see, thanks!

[Mario Carneiro]

some people prefer human readable proofs, some do write-only proofs, some golf proofs into the smallest number of lines of code or the shortest term proof

[Mario Carneiro]

this particular proof is going for a small term, it's just applying three lemmas with some very cleverly chosen instantiations

[Mario Carneiro]

it's probably not a very representative example of mathematics in mathlib, although mathlib is also not primarily focused on proof readability

[Mario Carneiro]

Usability of lemma statements and maintainability are the main criteria in mathlib IMO

[Utensil Song]

It seems proof style transfer could be a novel research topic for ML/AI, even better if it can help both directions:

• human readable proofs to more golfed proof (with measurable performance improvements)
• too golfed proof back to more readable proof (with minimal or no performance loss)

[Utensil Song]

A stretch bonus is style transfer to informal proofs.

[Mario Carneiro]

I would expect a symbolic tool to do better at golfing than AI

[Utensil Song]

Sure. IMHO ML based AI is more expected to improve quality of life (e.g. for researchers) rather than directly advance serious research.

[Mario Carneiro]

I would also expect a symbolic tool to do better at "unpacking" a proof, although ML would do better at summarizing the unpacked proof