Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2

dirichlet_eigenvalues_eq_nat_sq

Submitter: Kim Morrison.

Notes: Characterises the spectrum of the Dirichlet Laplacian on [0,pi]: lambda is an eigenvalue iff lambda = n^2 for some positive natural n.

Source: Classical Sturm-Liouville theory.

Informal solution: Case-split on the sign of lambda. For lambda <= 0 only the zero solution satisfies both boundary conditions. For lambda > 0 the general solution is A sin(sqrt lambda x) + B cos(sqrt lambda x); the boundary conditions force B = 0 and sqrt lambda in N_{>0}. Conversely, for lambda = n^2 with n in N_{>0}, the function sin(n x) is a nontrivial Dirichlet eigenfunction.

theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) :
    (∃ (y : ℝ → ℝ) (J : Set ℝ),
        IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
        (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧
        y 0 = 0 ∧ y Real.pi = 0 ∧
        ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔
      ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := bylam:ℝ⊢ (∃ y J,
    IsOpen J ∧
      Set.Icc 0 π ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
          (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔
  ∃ n, 0 < n ∧ lam = ↑n ^ 2
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 4, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 8, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 12, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026