[thaumasiotes]

> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4.

Well, I propose an alternative proof in lean4:

    import Mathlib.Tactic
    
    example (x y : ℝ)
      (h₁ : 2 * x + 3 * y = 10)
      (h₂ : 4 * x + 5 * y = 14)
      : x = -4 ∧ y = 6 := by
        have hy : y = 6 := by
          linear_combination 2 * h₁ - h₂
        have hx : x = -4 := by
          -- you'd think h₁ - 3 * hy would work, but it won't
          linear_combination 1/2 * h₁ - 3/2 * hy
        exact ⟨hx, hy⟩

---

One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs?

[litexlang]

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)

[thaumasiotes]

> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer.

I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example.

Before that, my first attempt at the lean proof looked like this:

    example (x y : ℝ)
        (h₁ : 2 * x + 3 * y = 10)
        (h₂ : 4 * x + 5 * y = 14)
        : x = -4 ∧ y = 6 := by
          -- double h₁ to cancel the x term
          have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁]
          conv at h₃ => ring_nf -- "ring normal form"
          -- subtract h₂ from h₃
          have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃]
          conv at h₄ => ring_nf
          conv at h₁ =>
            -- substitute y = 6 into h₁
            rw [h₄]
            ring_nf
          -- solve for x
          have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁]
          conv at h₅ => ring_nf
          apply And.intro h₅ h₄

> We are comparing Lean and Litex under conditions where they don’t rely too much on external packages

This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.

[c0balt]

> how are you supposed to do any nontrivial proofs?

One should also take a look at Isabelle/HOLs AFP here. You can get very far with Metis et al but it is very inefficient computationally.

Especially when proofs get larger and/or layer on abstractions (proving something nontrivial likely involves building on existing algorithms etc.) the ability to make proofs efficient to verify is important.

[litexlang]

``` If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs? ```

HAHA, what i am saying here is, each statement you write, is automatically checked by Litex, using its known specific facts and universal facts. Since any math proof, no matter complex or simple, can be divided into many small steps and each small step can be verified in that way, I guess it is fair to say "automatically figure out why they're correct" to a non-mathematicl person when introducing Litex.

[gus_massa]

How does it escale for NxN system? Let's say N=10 that is the maximal amount I'd write by hand (in exchange for a lot of money).

I took a look at the example and it's very intuitive. I'm trying to guess which heuristics is it using. Does it try to find exact matches of whatever is inside the parenthesis?

@GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

[thaumasiotes]

> @GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

Yes, there are several depending on what you want to do. The catchall is `simp` (short for 'simplify').

Why do we need more than one "do what I mean" command? (Or more than zero "do what I say" commands?) Because it's impossible to know what you mean. If you try to use a lot of `simp`, you'll notice that you often have to tell it what to do.

Note that what we really want for this problem is a linear algebra package that can do row reduction, not a formal prover. This problem is all arithmetic.