[FIELD NOTE]

Lean 3 syntax in Lean 4: the error messages that identify each holdover

@margaret-ashworth4 days ago▲ 1 net votes

lean4 · lean3 · mathlib · syntax · migration

If an answer or model output is in Lean 3 style, Lean v4.35.0 + Mathlib reports it with errors that don't say 'Lean 3'. Map from error to fix: unexpected token ','; expected '↦', '=>' means λ x, e, so write fun x ↦ e. Unknown identifier 'begin' plus Invalid 'end': There is no current scope to end means a begin … end block, so use by with indented tactics. unexpected token ','; expected '}' inside by { left, exact h } means comma-separated tactics, so use newlines or ;. unknown tactic plus 'The with keyword must be followed by a tactic or by an alternative' at cases h with hp hq means use obtain ⟨hp, hq⟩ := h, rcases, or cases h with | intro hp hq => …. Unknown identifier 'nat.add_zero' means lowercase Lean 3 namespaces, so capitalise (Nat.add_zero). unexpected token 'in'; expected ',' at ∑ i in s, f i is the older big-operator syntax, so write ∑ i ∈ s, f i. Then fix the names: many Lean 3-era lemma names were renamed or deleted, see posts on Mathlib renames.

2 COMMENTS

@jun-ho-park3 days ago
Reproduced all six on Lean/Mathlib v4.35.0, and the messages match word for word. Two small extras. The begin…end case also produces a third error, unexpected token ','; expected command, at the first comma-separated tactic. The by { left, exact h } case adds unsolved goals. Both fixes for cases ... with compile: cases h with | intro hp hq => exact hp and obtain ⟨hp, hq⟩ := h.
@margaret-ashworth2 days ago
More holdovers, tested 2026-11-01 on Lean/Mathlib v4.35.0, with the messages. split on a goal p ∧ q gives "Tactic split failed: Could not split an if or match expression in the goal": Lean 4's split is for if/match, so use constructor. refl, library_search, squeeze_simp, apply_instance and unfold_let each give a bare "unknown tactic" (plus "unsolved goals"); use rfl, exact?, simp? and infer_instance (I have not checked an equivalent for unfold_let). exact dec_trivial gives "Unknown identifier dec_trivial"; use decide. rw h gives "unexpected identifier; expected '['"; write rw [h]. by assume h, exact h gives "Unknown identifier h" plus "unexpected token ','; expected command"; use intro h. skip <|> trivial gives "unexpected token '<|>'; expected command"; there is no tactic-level <|>, so use first | t₁ | t₂. Three Lean 3 forms are still accepted with no warning: existsi 3, Mathlib's cases' h with n hn, and { tac } focusing blocks (with newline-separated tactics).