Symplectic matrices have determinant 1

symplectic_matrix_det — a formalization challenge from the lean-eval benchmark.

Notes

§39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For any commutative ring R and 2n × 2n symplectic matrix A over R (A * J * Aᵀ = J with J = [[0, -I], [I, 0]]), det A = 1. Taking determinants of AᵀJA = J only forces (det A)² = 1; the sign requires the Pfaffian argument. Mathlib has Matrix.symplecticGroup and proves symplectic_det (IsUnit (det A)) but the equals-1 claim is an explicit TODO in Mathlib/LinearAlgebra/SymplecticGroup.lean; no formalization of the identity was found in any other proof assistant.

Formal statement

/-- **Symplectic matrices have determinant 1.** For any commutative ring `R`
and `2n × 2n` symplectic matrix `A` over `R`, `A.det = 1`. -/
theorem symplectic_matrix_det
    {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
    {A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
    A.det = 1 := by
  sorry

Informal solution sketch

Apply the Pfaffian: for any 2n × 2n matrix M and antisymmetric 2n × 2n matrix Ω, Pf(Mᵀ Ω M) = det(M) · Pf(Ω). With Ω = J (so Pf(J) ≠ 0) and Aᵀ J A = J for A ∈ Sp_{2n}(R), one gets Pf(J) = det(A) · Pf(J), hence det A = 1. (This requires the Pfaffian for matrices over a commutative ring R; the construction is purely algebraic.)

Source

Folklore (Pfaffian computation). Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Marked as an open TODO at the head of Mathlib/LinearAlgebra/SymplecticGroup.lean (rev 5450b53e5ddc).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: symplectic_matrix_det
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.