Formalizing exceptional Lie algebra facts — draft feedback

Stream: new members

[Jonathan Reich]

Hi all,

I've started working on a Lean 4 project formalizing some basic structural facts
about the exceptional Lie algebras (G₂, F₄, E₆, E₇, E₈).

Right now the file includes:

• dimension and rank data,

• number of positive roots,

• basic inequalities (E₈ is largest by dim/rank),

• dimension decomposition 248 = 120 + 128,

• simple branching relations such as the E₈ → E₇ × SU(2) decomposition,

• some embedding index computations.

This is still an early draft, so I would appreciate any feedback on:

• idiomatic Lean usage,

• organization of the file,

• naming conventions,

• suggestions for how to connect to existing mathlib structures (e.g. LieAlgebra).

And here is the specific file I’d love feedback on:

/-
Copyright (c) 2025 Jonathan Reich. All rights reserved.
Released under Apache 2.0 license.
Authors: Jonathan Reich

# Exceptional Lie Algebras

This file contains facts about the five exceptional simple Lie algebras:
G₂, F₄, E₆, E₇, and E₈.

## Main Results

* Dimension and rank facts for all exceptional algebras
* Embedding chain E₆ ⊂ E₇ ⊂ E₈
* Dimension decomposition 248 = 120 + 128 for E₈
* Branching rules for E₈ → E₇ × SU(2)

## References

* Adams, "Lectures on Exceptional Lie Groups"
* Baez, "The Octonions"
-/

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

namespace ExceptionalLieAlgebras

/-- The five exceptional Lie algebras -/
inductive Exceptional where
  | G2 : Exceptional
  | F4 : Exceptional
  | E6 : Exceptional
  | E7 : Exceptional
  | E8 : Exceptional
deriving DecidableEq, Repr

/-- Dimension of exceptional Lie algebras -/
def Exceptional.dim : Exceptional → ℕ
  | G2 => 14
  | F4 => 52
  | E6 => 78
  | E7 => 133
  | E8 => 248

/-- Rank of exceptional Lie algebras -/
def Exceptional.rank : Exceptional → ℕ
  | G2 => 2
  | F4 => 4
  | E6 => 6
  | E7 => 7
  | E8 => 8

/-- Number of positive roots -/
def Exceptional.numPositiveRoots : Exceptional → ℕ
  | G2 => 6
  | F4 => 24
  | E6 => 36
  | E7 => 63
  | E8 => 120

-- Basic dimension facts

theorem dim_G2 : Exceptional.dim .G2 = 14 := rfl
theorem dim_F4 : Exceptional.dim .F4 = 52 := rfl
theorem dim_E6 : Exceptional.dim .E6 = 78 := rfl
theorem dim_E7 : Exceptional.dim .E7 = 133 := rfl
theorem dim_E8 : Exceptional.dim .E8 = 248 := rfl

theorem rank_G2 : Exceptional.rank .G2 = 2 := rfl
theorem rank_F4 : Exceptional.rank .F4 = 4 := rfl
theorem rank_E6 : Exceptional.rank .E6 = 6 := rfl
theorem rank_E7 : Exceptional.rank .E7 = 7 := rfl
theorem rank_E8 : Exceptional.rank .E8 = 8 := rfl

/-- E₈ is the largest exceptional algebra by dimension -/
theorem E8_largest_dim (e : Exceptional) : e.dim ≤ Exceptional.dim .E8 := by
  cases e <;> decide

/-- E₈ is the largest exceptional algebra by rank -/
theorem E8_largest_rank (e : Exceptional) : e.rank ≤ Exceptional.rank .E8 := by
  cases e <;> decide

/-- Dimension formula: dim = rank + 2 * numPositiveRoots -/
theorem dim_formula (e : Exceptional) : e.dim = e.rank + 2 * e.numPositiveRoots := by
  cases e <;> rfl

/-- E₈ dimension decomposition: 248 = 120 + 128
    This corresponds to SO(16) decomposition: adjoint + spinor -/
theorem E8_dim_decomposition : Exceptional.dim .E8 = 120 + 128 := rfl

/-- 120 = dim(SO(16)) adjoint representation -/
def dim_SO16_adjoint : ℕ := 120

/-- 128 = dim(SO(16)) spinor representation -/
def dim_SO16_spinor : ℕ := 128

theorem SO16_decomposition : dim_SO16_adjoint + dim_SO16_spinor = 248 := rfl

/-- E₇ embeds in E₈ with complement SU(2) -/
theorem E8_E7_embedding : Exceptional.dim .E8 = Exceptional.dim .E7 + 3 + 112 := by
  -- 248 = 133 + 3 + 112, where 3 = dim(SU(2)), 112 = (56, 2) representation
  rfl

/-- The 56-dimensional fundamental representation of E₇ -/
def E7_fundamental_dim : ℕ := 56

/-- E₇ branching: 248 → (133, 1) ⊕ (1, 3) ⊕ (56, 2) -/
theorem E8_to_E7_SU2_branching :
    Exceptional.dim .E8 = Exceptional.dim .E7 * 1 + 1 * 3 + E7_fundamental_dim * 2 := by
  -- 248 = 133 + 3 + 112
  rfl

/-- E₆ embeds in E₇ -/
theorem E7_E6_embedding : Exceptional.dim .E7 > Exceptional.dim .E6 := by decide

/-- The 27-dimensional fundamental representation of E₆ -/
def E6_fundamental_dim : ℕ := 27

/-- E₈ → E₆ × SU(3) branching: 248 → (78,1) ⊕ (1,8) ⊕ (27,3) ⊕ (27̄,3̄) -/
theorem E8_to_E6_SU3_branching :
    Exceptional.dim .E8 = 78 + 8 + 27 * 3 + 27 * 3 := by
  -- 248 = 78 + 8 + 81 + 81
  rfl

/-- The (27,3) term in E₈ → E₆ × SU(3) gives 3 generations -/
theorem three_generations_from_E8 : 27 * 3 = 81 := rfl

/-- Dimension chain: E₆ < E₇ < E₈ -/
theorem exceptional_E_chain :
    Exceptional.dim .E6 < Exceptional.dim .E7 ∧
    Exceptional.dim .E7 < Exceptional.dim .E8 := by
  constructor <;> decide

/-- Rank chain: rank(E₆) < rank(E₇) < rank(E₈) -/
theorem exceptional_E_rank_chain :
    Exceptional.rank .E6 < Exceptional.rank .E7 ∧
    Exceptional.rank .E7 < Exceptional.rank .E8 := by
  constructor <;> decide

/-- G₂ is the automorphism group of the octonions -/
-- This is stated as a definition; the proof would require octonion theory
def G2_is_Oct_Aut : Prop := Exceptional.dim .G2 = 14

/-- F₄ is the automorphism group of the exceptional Jordan algebra -/
def F4_is_Jordan_Aut : Prop := Exceptional.dim .F4 = 52

/-- The dual Coxeter number of exceptional algebras -/
def Exceptional.dualCoxeter : Exceptional → ℕ
  | G2 => 4
  | F4 => 9
  | E6 => 12
  | E7 => 18
  | E8 => 30

theorem dualCoxeter_G2 : Exceptional.dualCoxeter .G2 = 4 := rfl
theorem dualCoxeter_F4 : Exceptional.dualCoxeter .F4 = 9 := rfl
theorem dualCoxeter_E6 : Exceptional.dualCoxeter .E6 = 12 := rfl
theorem dualCoxeter_E7 : Exceptional.dualCoxeter .E7 = 18 := rfl
theorem dualCoxeter_E8 : Exceptional.dualCoxeter .E8 = 30 := rfl

/-- E₈ has the largest dual Coxeter number among exceptional algebras -/
theorem E8_largest_dualCoxeter (e : Exceptional) :
    e.dualCoxeter ≤ Exceptional.dualCoxeter .E8 := by
  cases e <;> decide

/-- E₈ is self-dual: its adjoint representation equals its smallest fundamental -/
theorem E8_self_dual : Exceptional.dim .E8 = 248 := rfl

/-- The index of embedding E₇ ⊂ E₈ -/
def E7_in_E8_index : ℕ := Exceptional.dim .E8 - Exceptional.dim .E7

theorem E7_in_E8_index_value : E7_in_E8_index = 115 := rfl

/-- The index of embedding E₆ ⊂ E₇ -/
def E6_in_E7_index : ℕ := Exceptional.dim .E7 - Exceptional.dim .E6

theorem E6_in_E7_index_value : E6_in_E7_index = 55 := rfl

end ExceptionalLieAlgebras

Thanks in advance for any guidance — happy to iterate

[Weiyi Wang]

Sorry to be blunt but this looks like just some natural number arithmetic hidden behind names?

[Aaron Liu]

you've written a lot of numbers and you have a lot of equations

[Aaron Liu]

but you haven't related them to the Lie algebras at all

[Jonathan Reich]

yep, totally fair point. This file is just a warm-up. right now,I’m setting up the basic constants and branching-rule arithmetic before moving on to the actual Lie algebra structures (root systems, embeddings, representations). Right now it is just numerical bookkeeping; the deeper formalization will come in later files once I get more familiar with the mathlib APIs.

[Michael Rothgang]

Please read #backticks for formatting your Lean code: that makes it much nicer to read. I usually don't give feedback on unformatted code, but #backticks make is so much easier to do.

[Jonathan Reich]

Michael Rothgang said:

Please read #backticks for formatting your Lean code: that makes it much nicer to read. I usually don't give feedback on unformatted code, but #backticks make is so much easier to do.

thanks for letting me know. edited it. And yeah, if you do have any feedback, that would be appreciated.
working on my next proof.

[Bryan Wang]

You might be interested in taking a look at Mathlib.Algebra.Lie.CartanMatrix and building upon that.

[Jonathan Reich]

@Bryan Wang
I've put together a PR adding Cartan matrices for the classical types A, B, C, D.
It follows the existing pattern from the exceptional algebras
https://github.com/leanprover-community/mathlib4/pull/32763
Would appreciate your feedback whenever suits you.