New to Lean 4—where to find a “syntax dictionary” or practic

Stream: lean4

[Ceiling Ge]

Hello everyone,
I’m a complete newcomer to Lean 4—I’ve been learning it for about a week. I’ve tried the Natural Number Game and really like that approach, but I’m also looking for a project-driven way to learn. Specifically, I found a task that involves proving certain theorems in Lean 4, which mathematically I understand, but in Lean 4 code I keep running into syntax/indentation issues and other compilation errors.

ChatGPT has helped me somewhat, but it often fails to fix my final errors in a correct or fully working form. I suspect I need a more thorough resource or “dictionary” of Lean 4 syntax—some place I can quickly look up each concept’s usage, or a tutorial focusing on the typical code structure, by blocks, calc blocks, indentation rules, and how to interpret compiler messages.

My mathematical understanding is fine; it’s purely the Lean 4 coding style that trips me up. Below is a snippet of a proof I’m working on (pinned to Lean 4.5.0-rc1, mathlib commit 8f013c4...). I’d love advice on any recommended reading or reference that’s more “task-oriented”.

-- Lean 4 and Mathlib Versions: This project uses Lean 4 version 4.5.0-rc1 (installed via elan) and pins Mathlib4 to commit 8f013c457aea2ea1b0156c0c98043c9ed018529f.
-- by Ceiling Ge


import Mathlib
open scoped BigOperators
-- Lean 4 demo: Prove that there is a k such that
--   a₀ + a₁ x + ... + aₙ xⁿ ≤ a₀ + a₁ + ... + aₖ
-- for all x in [0, 1].


/--

  We want to prove the following statement:

  "Given a finite sequence of real numbers a₀, a₁, ..., aₙ,
   there exists some index k (0 ≤ k ≤ n) such that for every x ∈ [0,1],
   the polynomial a₀ + a₁ x + ... + aₙ xⁿ
   is at most the partial sum a₀ + a₁ + ... + aₖ."

  The proof proceeds by:
  1) Defining partial sums Sᵢ = ∑(j=0 to i) aⱼ.
  2) Selecting k for which Sₖ is the maximum among all partial sums.
  3) Rewriting the polynomial using Abel’s summation (or a similar factorization),
     showing that for x in [0,1] each term is bounded above by Sₖ.
  4) Concluding the inequality holds for that k and all x ∈ [0,1].
-/
theorem exists_partial_sum_bound
  (n : ℕ)
  (a : Fin (n+1) → ℝ) :
  ∃ (k : Fin (n+1)), ∀ (x : ℝ), (0 ≤ x ∧ x ≤ 1) →
    (∑ i in Finset.range (n+1), a i * x^i) ≤ (∑ i in Finset.range (k+1), a i) := by
-- Step 1: 定义 S(i) = a₀ + ... + aᵢ
let S : ℕ → ℝ := fun i => ∑ j in Finset.range (i+1), a j
-- Step 2: 在 i = 0..n 里找 S(i) 的最大值
let indexSet := Finset.range (n+1)
-- 需要先证明它非空:
have h_nonempty : Finset.Nonempty indexSet := by
  use 0
  simp [Finset.mem_range]
-- 用 sup' 取最大值
let M := indexSet.sup' h_nonempty (fun i => S i)
-- 用 exists_mem_eq_sup' 拿到“实现最大值”的下标 maxIndex
obtain ⟨maxIndex, h_mem, h_eq⟩ :=
  indexSet.exists_mem_eq_sup' h_nonempty (fun i => S i)
  <;> simp
-- maxIndex 是 ℕ 类型，并且 maxIndex ∈ {0,1,...,n}
-- 若你后面需要 k : Fin (n+1)，可以这样转换:
let k : Fin (n+1) := ⟨maxIndex, Finset.mem_range.mp h_mem⟩
use k
-- 此时:
-- 1) maxIndex ∈ indexSet，且 S(maxIndex) = M
-- 2) k 就是“使 S(i) 最大”的那个下标(以 Fin(n+1) 表示)
-- 你可以后续用 h_eq : S(maxIndex) = M 来做进一步证明。
  -- A small lemma: for all i in 0..n, S i ≤ S k
have S_le_Sk : ∀ i : ℕ, i ≤ n → S i ≤ S k := by
    intro i hi
    exact Finset.le_argmax_of_mem_argmax (Finset.mem_range.2 (Nat.lt_succ_of_le hi)) _

  ----------------------------------------------------------------
  -- Step 3: Rewrite a₀ + a₁ x + ... + aₙ xⁿ via a standard “Abel-type” factorization.
  --
  -- The key identity (Abel's Summation Trick) can be shown by
  -- telescoping or direct finite-sum manipulation.
  --
  --  ∑(i=0 to n) [aᵢ * x^i]
  --  = [S n * x^n] + ∑(i=0 to n-1) [S i * (x^i - x^(i+1))].
  --
  -- We'll prove a small lemma for that decomposition.
  ----------------------------------------------------------------
have abel_decomposition :
    ∑ i in Finset.range (n+1), (a i * x^i)
    = S n * x^n + ∑ i in Finset.range n, (S i * (x^i - x^(i+1))) := by

    -- Proof by induction or by direct summation manipulation.
    -- Here we do a short telescoping argument:

    calc
      ∑ i in Finset.range (n+1), a i * x^i
    = ∑ i in Finset.range (n+1), (S i - S (i-1)) * x^i : by

          apply Finset.sum_congr rfl
          intro i hi
          cases i with
          | mk iVal =>
            -- iVal is a natural, so we interpret S(iVal) - S(iVal-1)
            -- but for iVal=0, S(-1) can be taken as 0 by convention.
            have : S iVal - S (iVal - 1) = a iVal := by
              if h : iVal = 0 then
                -- then S(iVal - 1) = S(-1) = 0
                simp [h, S]
              else
                let iPred := iVal - 1
                simp [S]
                -- partial_sum (iVal) - partial_sum (iVal-1) = a_{iVal}.
            rw [this]
      -- Now write each term partial_sum(i)*x^i in an Abel-like shape:
      _ = ∑ i in Finset.range (n+1),
            (S i * x^i) - (S (i-1) * x^i)
        : by
          apply Finset.sum_congr rfl
          intro i hi
          rw [mul_sub, sub_mul]
      -- We telescope in pairs:
      _ = (S n * x^n)
          + ∑ i in Finset.range n, (S i * x^i) - (S i * x^(i+1))
        : by
          -- separate out the i=n term and group the rest
          rw [Finset.sum_range_succ']
          simp
      _ = S n * x^n
          + ∑ i in Finset.range n, S i * (x^i - x^(i+1))
        : by
          apply Finset.sum_congr rfl
          intro i hi
          ring
    -- done
    ----------------------------------------------------------------
  -- Step 4: Use the decomposition + the fact S i ≤ S k and (x^i - x^(i+1)) ≥ 0 (x in [0,1]).
  --         Summation then bounds the whole polynomial by S k.
  ----------------------------------------------------------------
  intro x hx
  -- hx = (0 ≤ x ∧ x ≤ 1)
  let h0 := hx.left
  let h1 := hx.right

  -- First, apply the Abel decomposition lemma:
  rw [abel_decomposition]

  -- We have: ∑ i aᵢ x^i = S n * x^n + ∑ i=0..n-1 [S i * (x^i - x^(i+1))].
  -- Since 0 ≤ x ≤ 1, we know 0 ≤ x^n ≤ 1 and 0 ≤ (x^i - x^(i+1)) for i=0..n-1.
  -- Also S i ≤ S k by construction. So each piece is ≤ S k times the same factor.

  -- Bound the first big term: S n * x^n ≤ S k * x^n
  have term1 : S n * x^n ≤ S k * x^n := by
    apply mul_le_mul_of_nonneg_right (S_le_Sk n (le_refl _)) (by positivity)

  -- Bound the summation part term by term.
  have term2 : ∑ i in Finset.range n, S i * (x^i - x^(i+1))
             ≤ ∑ i in Finset.range n, S k * (x^i - x^(i+1)) := by
    apply Finset.sum_le_sum
    intro i hi
    apply mul_le_mul_of_nonneg_right (S_le_Sk i (Finset.mem_range.mp hi).le) _
    -- x^i - x^(i+1) = x^i(1 - x), which is ≥ 0 if 0 ≤ x ≤ 1
    calc x^i - x^(i+1) = x^i * (1 - x) ≥ 0 : by
      apply mul_nonneg
      · exact Real.pow_nonneg h0 i
      · exact sub_nonneg_of_le h1

  -- Combine the bounds
  calc
    S n * x^n + ∑ i in Finset.range n, S i * (x^i - x^(i+1))
    ≤ (S k * x^n) + ∑ i in Finset.range n, S k * (x^i - x^(i+1))
      : add_le_add term1 term2
    _ = S k * x^n + S k * ∑ i in Finset.range n, (x^i - x^(i+1))
      : by rw [Finset.sum_mul]
    _ = S k * [ x^n + ∑ i in Finset.range n, (x^i - x^(i+1)) ]
      : by ring
    -- Now note that the inside sums telescope from x^0 = 1 down to x^n:
    _ = S k * [1]  -- Because x^0=1, and ∑(x^i - x^(i+1)) = 1 - x^n
      : by
        rw [Finset.sum_range_sub']
        simp [← Finset.sum_range_succ, Nat.succ_eq_add_one]
        ring
    _ = S k
      : by simp

  -- Hence ∑ i=0..n aᵢ x^i ≤ S k, i.e. the polynomial is bounded by that partial sum.
  -- This completes the proof.
```

```

Any pointers on bridging the gap—so I can confidently handle these syntax errors—would be greatly appreciated. Thank you so much!

[suhr]

The main resources I would use are Theorem Proving in Lean 4, The Lean Language Reference and Mathlib documentation. There's also Loogle and tactics like exact?, apply? and rw?.

You also might find interesting my own book, Типизированная математика.

By the way, errors in your code are not syntactical: you try to use simp with a lemma that is not applicable to the goal, use a lemma that does not exists (Finset.le_argmax_of_mem_argmax) and use a variable without introducing it anywhere (x).

[suhr]

There're some syntax errors as well though, for example the syntax of calc is different and indentation is not always consistent. And there are some type errors.

[Sabbir Rahman]

chatgpt keep mixing lean3 and lean4, my suggestions would be to read up on any tactic you get from chatgpt to be sure what that tactic exactly do

[suhr]

As a general advice, never copypaste ChatGPT (or Deepseek or whatever) code. Pin it as a reference to a half of a screen and then write the code yourself. This way you have the opportunity to learn and to avoid mysterious "syntax errors".

Lean is an interactive proof assistant, use this interactivity to your advantage.

[Patrick Massot]

Really the main advice is to stop using LLM and try to learn instead. Every other advice is less important. If you already know some math then the resource meant for you is #mil.

[Ceiling Ge]

Thank you! The books looks so goood. Did you wrote the book while learning?

[Ceiling Ge]

:rolling_on_the_floor_laughing: yes, there are many errors…

[Ceiling Ge]

@suhr Thank you! The books looks so goood. Did you wrote the book while learning?

@suhr @Patrick Massot @Sabbir Rahman Yes, Definitely, I should spend more time reading and talking in this forum.

[suhr]

Ceiling Ge said:

Thank you! The books looks so goood. Did you wrote the book while learning?

No, there was a much shorter tutorial for Isabelle/HOL and Lean 3 before this book.
The whole project emerged from realization that mathematical texts do not work for non-mathematicians, and if I really want to make mathematics more accessible for mere mortals (programmers), I should start from the ground up (like, really, without assuming that readers already think like mathematicians) and build a course around a theorem prover.
I'm definitely not the best writer, so I guess the book requires quite a bit of editing. :smile: Pull requests are welcome.