Created
May 2, 2026 12:02
-
-
Save kim-em/c035f0a8f6b4ee057436e99349b13506 to your computer and use it in GitHub Desktop.
lean-eval Aristotle (Harmonic) submission for dirichlet_eigenvalues_eq_nat_sq
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| open scoped Real | |
| theorem 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 := by | |
| sorry |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "challenge_module": "Challenge", | |
| "solution_module": "Solution", | |
| "theorem_names": [ | |
| "dirichlet_eigenvalues_eq_nat_sq" | |
| ], | |
| "permitted_axioms": [ | |
| "propext", | |
| "Quot.sound", | |
| "Classical.choice" | |
| ], | |
| "enable_nanoda": false | |
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| namespace Submission.Helpers | |
| end Submission.Helpers |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name = "dirichlet_eigenvalues_eq_nat_sq" | |
| testDriver = "workspace_test" | |
| defaultTargets = ["Challenge", "Solution", "Submission"] | |
| [leanOptions] | |
| autoImplicit = false | |
| [[require]] | |
| name = "mathlib" | |
| git = "https://github.com/leanprover-community/mathlib4.git" | |
| rev = "5450b53e5ddc" | |
| [[lean_lib]] | |
| name = "Challenge" | |
| [[lean_lib]] | |
| name = "Solution" | |
| [[lean_lib]] | |
| name = "Submission" | |
| [[lean_exe]] | |
| name = "workspace_test" | |
| root = "WorkspaceTest" |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| leanprover/lean4:v4.30.0-rc2 | |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| import Submission | |
| open scoped Real | |
| theorem 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 := by | |
| exact Submission.dirichlet_eigenvalues_eq_nat_sq lam |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| open scoped Real | |
| open Set Real | |
| namespace Submission | |
| /-! ## Backward direction -/ | |
| private lemma backward_direction (lam : ℝ) : | |
| (∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2) → | |
| (∃ (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) := by | |
| rintro ⟨ n, hn, rfl ⟩; | |
| refine' ⟨ fun x => Real.sin ( n * x ), Set.univ, isOpen_univ, Set.subset_univ _, _, _, _, _ ⟩ <;> norm_num; | |
| · fun_prop; | |
| · unfold deriv; | |
| norm_num [ fderiv_apply_one_eq_deriv, mul_comm ]; | |
| intro x; convert HasDerivAt.const_mul ( n : ℝ ) ( HasDerivAt.cos ( hasDerivAt_mul_const _ ) ) using 1; ring; | |
| · exact ⟨ Real.pi / 2 / n, ⟨ by positivity, by rw [ div_lt_iff₀ ( by positivity ) ] ; nlinarith [ Real.pi_pos, show ( n : ℝ ) ≥ 1 by norm_cast ] ⟩, by rw [ mul_div_cancel₀ _ ( by positivity ) ] ; norm_num ⟩ | |
| /-! ## Forward direction -/ | |
| private lemma forward_direction (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) := by | |
| intro h | |
| obtain ⟨y, J, hJ_open, hJ_subset, hJ_deriv1, hJ_deriv2, hy0, hyπ, hx⟩ := h | |
| have h_lam_nonneg : 0 ≤ lam := by | |
| -- By integration by parts, we have $\int_0^\pi (y')^2 \, dx = \int_0^\pi \lambda y^2 \, dx$. | |
| have h_int_parts : ∫ x in (0 : ℝ)..Real.pi, (deriv y x) ^ 2 = ∫ x in (0 : ℝ)..Real.pi, lam * y x ^ 2 := by | |
| have h_int_parts : ∀ a b, 0 ≤ a → a ≤ b → b ≤ Real.pi → ∫ x in a..b, deriv y x * deriv y x = (deriv y b) * y b - (deriv y a) * y a - ∫ x in a..b, y x * deriv (deriv y) x := by | |
| intros a b _ _ _; rw [ intervalIntegral.integral_mul_deriv_eq_deriv_mul ]; | |
| congr! 1; | |
| exact intervalIntegral.integral_congr fun x _ => mul_comm _ _; | |
| · exact fun x hx => hasDerivAt_deriv_iff.mpr ( show DifferentiableAt ℝ ( deriv y ) x from by exact HasDerivAt.differentiableAt ( hJ_deriv2 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) ); | |
| · exact fun x hx => hJ_deriv1 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith; | |
| · apply_rules [ ContinuousOn.intervalIntegrable ]; | |
| exact ContinuousOn.congr ( show ContinuousOn ( fun x => - ( lam * y x ) ) ( uIcc a b ) from ContinuousOn.neg ( ContinuousOn.mul continuousOn_const <| continuousOn_of_forall_continuousAt fun x hx => HasDerivAt.continuousAt <| hJ_deriv1 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) ) fun x hx => HasDerivAt.deriv <| hJ_deriv2 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith; | |
| · apply_rules [ ContinuousOn.intervalIntegrable ]; | |
| exact continuousOn_of_forall_continuousAt fun x hx => HasDerivAt.continuousAt ( hJ_deriv2 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ); | |
| simp_all +decide [ sq, mul_assoc, mul_comm, mul_left_comm ]; | |
| rw [ h_int_parts 0 Real.pi le_rfl Real.pi_pos.le le_rfl ] ; norm_num [ hy0, hyπ ]; | |
| rw [ ← intervalIntegral.integral_const_mul ] ; rw [ ← intervalIntegral.integral_neg ] ; refine' intervalIntegral.integral_congr fun x hx => _ ; rw [ hJ_deriv2 x ( hJ_subset <| by simpa [ Real.pi_pos.le ] using hx ) |> HasDerivAt.deriv ] ; ring; | |
| -- Since $y$ is not identically zero on $(0, \pi)$, we have $\int_0^\pi y^2 \, dx > 0$. | |
| have h_int_pos : 0 < ∫ x in (0 : ℝ)..Real.pi, y x ^ 2 := by | |
| rw [ intervalIntegral.integral_of_le Real.pi_pos.le ]; | |
| rw [ MeasureTheory.integral_pos_iff_support_of_nonneg ]; | |
| · obtain ⟨ x, hx₁, hx₂ ⟩ := hx; have := hJ_deriv1 x ( hJ_subset <| Set.Ioo_subset_Icc_self hx₁ ) ; have := this.continuousAt; simp_all +decide [ Function.support ] ; | |
| -- Since $y$ is continuous at $x$ and $y(x) \neq 0$, there exists an interval $(a, b)$ around $x$ where $y$ is non-zero. | |
| obtain ⟨a, b, ha, hb, hab⟩ : ∃ a b : ℝ, 0 ≤ a ∧ a < b ∧ b ≤ Real.pi ∧ ∀ x ∈ Set.Ioo a b, y x ≠ 0 := by | |
| have := Metric.continuousAt_iff.mp this; | |
| obtain ⟨ δ, δ_pos, H ⟩ := this ( |y x| ) ( abs_pos.mpr hx₂ ) ; exact ⟨ x, x + Min.min δ ( Real.pi - x ), by linarith, by linarith [ lt_min δ_pos ( sub_pos.mpr hx₁.2 ) ], by linarith [ min_le_left δ ( Real.pi - x ), min_le_right δ ( Real.pi - x ) ], fun z hz => by cases abs_cases ( y x ) <;> linarith [ abs_lt.mp ( H ( show |z - x| < δ from abs_lt.mpr ⟨ by linarith [ hz.1, min_le_left δ ( Real.pi - x ) ], by linarith [ hz.2, min_le_left δ ( Real.pi - x ) ] ⟩ ) ) ] ⟩ ; | |
| exact lt_of_lt_of_le ( by simpa [ hb.le ] ) ( MeasureTheory.measure_mono <| show Set.Ioo a b ⊆ { x | ¬y x = 0 } ∩ Ioc 0 Real.pi from fun x hx => ⟨ hab.2 x hx, ⟨ by linarith [ hx.1 ], by linarith [ hx.2 ] ⟩ ⟩ ); | |
| · exact fun x => sq_nonneg _; | |
| · exact ContinuousOn.integrableOn_Icc ( by exact ContinuousOn.pow ( by exact continuousOn_of_forall_continuousAt fun x hx => HasDerivAt.continuousAt ( hJ_deriv1 x ( hJ_subset hx ) ) ) _ ) |> fun h => h.mono_set ( Set.Ioc_subset_Icc_self ); | |
| norm_num at *; nlinarith [ show 0 ≤ ∫ x in ( 0 : ℝ )..Real.pi, deriv y x ^ 2 by exact intervalIntegral.integral_nonneg ( by positivity ) fun x hx => sq_nonneg _ ] ; | |
| by_cases h_lam_zero : lam = 0; | |
| · -- Since $y'' = 0$, we have $y' = C$ for some constant $C$. | |
| obtain ⟨C, hC⟩ : ∃ C : ℝ, ∀ x ∈ Set.Icc 0 Real.pi, deriv y x = C := by | |
| have h_const_deriv : ∀ a b : ℝ, a ∈ Set.Icc 0 Real.pi → b ∈ Set.Icc 0 Real.pi → ∫ x in a..b, deriv (deriv y) x = deriv y b - deriv y a := by | |
| intros a b ha hb; | |
| rw [ intervalIntegral.integral_deriv_eq_sub' ]; | |
| · rfl; | |
| · exact fun x hx => HasDerivAt.differentiableAt ( hJ_deriv2 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith [ ha.1, ha.2, hb.1, hb.2 ] ); | |
| · exact ContinuousOn.congr ( show ContinuousOn ( fun _ => 0 ) _ from continuousOn_const ) fun x hx => by simpa [ h_lam_zero ] using HasDerivAt.deriv ( hJ_deriv2 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith [ ha.1, ha.2, hb.1, hb.2 ] ) ; | |
| use deriv y 0; | |
| intro x hx; specialize h_const_deriv 0 x; simp_all +decide [ intervalIntegral.integral_of_le ] ; | |
| exact eq_of_sub_eq_zero ( h_const_deriv Real.pi_pos.le ▸ MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero fun t ht => HasDerivAt.deriv ( hJ_deriv2 t ( hJ_subset <| by constructor <;> linarith [ ht.1, ht.2 ] ) ) ); | |
| -- Since $y' = C$, we have $y = Cx + D$ for some constant $D$. | |
| have h_y_linear : ∀ x ∈ Set.Icc 0 Real.pi, y x = C * x + y 0 := by | |
| have h_y_linear : ∀ a b : ℝ, 0 ≤ a → a ≤ b → b ≤ Real.pi → ∫ x in a..b, deriv y x = y b - y a := by | |
| intros a b _ _ _; rw [ intervalIntegral.integral_deriv_eq_sub' ] <;> norm_num; | |
| · exact fun x hx => HasDerivAt.differentiableAt ( hJ_deriv1 x <| hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ); | |
| · exact ContinuousOn.congr ( continuousOn_const ) fun x hx => hC x ⟨ by cases Set.mem_uIcc.mp hx <;> linarith, by cases Set.mem_uIcc.mp hx <;> linarith ⟩; | |
| intro x hx; have := h_y_linear 0 x le_rfl hx.1 hx.2; rw [ intervalIntegral.integral_congr fun t ht => hC t <| by constructor <;> cases Set.mem_uIcc.mp ht <;> linarith [ hx.1, hx.2 ] ] at this; norm_num at this; linarith; | |
| grind +revert; | |
| · -- For lam > 0, show y = A*sin(√lam*x) + B*cos(√lam*x) on [0,π]. | |
| have h_y_form : ∃ A B : ℝ, ∀ x ∈ Set.Icc 0 Real.pi, y x = A * Real.sin (Real.sqrt lam * x) + B * Real.cos (Real.sqrt lam * x) := by | |
| -- Define $f(x) = y(x) \cos(\sqrt{\lambda} x) - \frac{y'(x)}{\sqrt{\lambda}} \sin(\sqrt{\lambda} x)$ and $g(x) = y(x) \sin(\sqrt{\lambda} x) + \frac{y'(x)}{\sqrt{\lambda}} \cos(\sqrt{\lambda} x)$. | |
| set f : ℝ → ℝ := fun x => y x * Real.cos (Real.sqrt lam * x) - (deriv y x) / Real.sqrt lam * Real.sin (Real.sqrt lam * x) | |
| set g : ℝ → ℝ := fun x => y x * Real.sin (Real.sqrt lam * x) + (deriv y x) / Real.sqrt lam * Real.cos (Real.sqrt lam * x); | |
| -- Show that $f$ and $g$ are constant on $[0, \pi]$. | |
| have h_f_const : ∀ x ∈ Set.Icc 0 Real.pi, deriv f x = 0 := by | |
| intro x hx; | |
| convert HasDerivAt.deriv ( HasDerivAt.sub ( HasDerivAt.mul ( hJ_deriv1 x ( hJ_subset hx ) ) ( HasDerivAt.cos ( HasDerivAt.const_mul ( Real.sqrt lam ) ( hasDerivAt_id x ) ) ) ) ( HasDerivAt.mul ( HasDerivAt.div_const ( hJ_deriv2 x ( hJ_subset hx ) ) _ ) ( HasDerivAt.sin ( HasDerivAt.const_mul ( Real.sqrt lam ) ( hasDerivAt_id x ) ) ) ) ) using 1 | |
| field_simp | |
| ring | |
| rw [ Real.sq_sqrt ] <;> linarith! | |
| have h_g_const : ∀ x ∈ Set.Icc 0 Real.pi, deriv g x = 0 := by | |
| intro x hx; | |
| convert HasDerivAt.deriv ( HasDerivAt.add ( HasDerivAt.mul ( hJ_deriv1 x ( hJ_subset hx ) ) ( HasDerivAt.sin ( HasDerivAt.const_mul ( Real.sqrt lam ) ( hasDerivAt_id x ) ) ) ) ( HasDerivAt.mul ( HasDerivAt.div_const ( hJ_deriv2 x ( hJ_subset hx ) ) _ ) ( HasDerivAt.cos ( HasDerivAt.const_mul ( Real.sqrt lam ) ( hasDerivAt_id x ) ) ) ) ) using 1 ; ring; | |
| -- Combine like terms and simplify the expression. | |
| field_simp | |
| ring; | |
| rw [ Real.sq_sqrt ] <;> linarith!; | |
| -- Since $f$ and $g$ are constant on $[0, \pi]$, we have $f(x) = f(0)$ and $g(x) = g(0)$ for all $x \in [0, \pi]$. | |
| have h_f_eq_f0 : ∀ x ∈ Set.Icc 0 Real.pi, f x = f 0 := by | |
| have h_f_eq_f0 : ∀ a b, 0 ≤ a → a ≤ b → b ≤ Real.pi → ∫ x in a..b, deriv f x = f b - f a := by | |
| intros a b _ _ _; rw [ intervalIntegral.integral_deriv_eq_sub' ] <;> norm_num; | |
| · exact fun x hx => DifferentiableAt.sub ( DifferentiableAt.mul ( hJ_deriv1 x ( hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) |> HasDerivAt.differentiableAt ) ( DifferentiableAt.cos ( differentiableAt_id.const_mul _ ) ) ) ( DifferentiableAt.mul ( DifferentiableAt.div_const ( hJ_deriv2 x ( hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) |> HasDerivAt.differentiableAt ) _ ) ( DifferentiableAt.sin ( differentiableAt_id.const_mul _ ) ) ); | |
| · exact ContinuousOn.congr ( show ContinuousOn ( fun _ => 0 ) _ from continuousOn_const ) fun x hx => h_f_const x ⟨ by cases Set.mem_uIcc.mp hx <;> linarith, by cases Set.mem_uIcc.mp hx <;> linarith ⟩; | |
| intro x hx; specialize h_f_eq_f0 0 x le_rfl hx.1 hx.2; rw [ intervalIntegral.integral_congr fun t ht => h_f_const t <| by constructor <;> cases Set.mem_uIcc.mp ht <;> linarith [ hx.1, hx.2 ] ] at h_f_eq_f0; norm_num at * ; linarith; | |
| have h_g_eq_g0 : ∀ x ∈ Set.Icc 0 Real.pi, g x = g 0 := by | |
| have h_g_eq_g0 : ∀ a b, 0 ≤ a → a ≤ b → b ≤ Real.pi → ∫ x in a..b, deriv g x = g b - g a := by | |
| intros a b _ _ _; rw [ intervalIntegral.integral_deriv_eq_sub' ] <;> norm_num; | |
| · exact fun x hx => DifferentiableAt.add ( DifferentiableAt.mul ( hJ_deriv1 x ( hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) |> HasDerivAt.differentiableAt ) ( DifferentiableAt.sin ( differentiableAt_id.const_mul _ ) ) ) ( DifferentiableAt.mul ( DifferentiableAt.div_const ( hJ_deriv2 x ( hJ_subset <| by constructor <;> cases Set.mem_uIcc.mp hx <;> linarith ) |> HasDerivAt.differentiableAt ) _ ) ( DifferentiableAt.cos ( differentiableAt_id.const_mul _ ) ) ); | |
| · exact ContinuousOn.congr ( show ContinuousOn ( fun _ => 0 ) _ from continuousOn_const ) fun x hx => h_g_const x ⟨ by cases Set.mem_uIcc.mp hx <;> linarith, by cases Set.mem_uIcc.mp hx <;> linarith ⟩; | |
| intro x hx; specialize h_g_eq_g0 0 x le_rfl hx.1 hx.2; rw [ intervalIntegral.integral_congr fun t ht => h_g_const t <| by constructor <;> cases Set.mem_uIcc.mp ht <;> linarith [ hx.1, hx.2 ] ] at h_g_eq_g0; norm_num at * ; linarith; | |
| use g 0, f 0; | |
| intro x hx; rw [ ← h_f_eq_f0 x hx, ← h_g_eq_g0 x hx ] ; ring; | |
| linear_combination -Real.sin_sq_add_cos_sq ( Real.sqrt lam * x ) * y x; | |
| -- Apply boundary conditions to find A and B. | |
| obtain ⟨A, B, h_y⟩ := h_y_form | |
| have hB : B = 0 := by | |
| simpa [ h_y 0 ⟨ by norm_num, Real.pi_pos.le ⟩ ] using hy0 | |
| have hA : A ≠ 0 := by | |
| grind | |
| have h_sin_zero : Real.sin (Real.sqrt lam * Real.pi) = 0 := by | |
| grind; | |
| -- Since $\sin(\sqrt{\lambda} \pi) = 0$, we have $\sqrt{\lambda} \pi = n \pi$ for some integer $n$, implying $\sqrt{\lambda} = n$. | |
| obtain ⟨n, hn⟩ : ∃ n : ℤ, Real.sqrt lam = n := by | |
| exact Real.sin_eq_zero_iff.mp h_sin_zero |> fun ⟨ n, hn ⟩ => ⟨ n, by nlinarith [ Real.pi_pos ] ⟩; | |
| exact ⟨ n.natAbs, Int.natAbs_pos.mpr ( show n ≠ 0 by rintro rfl; exact h_lam_zero <| by norm_num at hn; nlinarith [ Real.mul_self_sqrt h_lam_nonneg ] ), by simp +decide [ ← @Nat.cast_inj ℝ, ← hn, Real.sq_sqrt h_lam_nonneg ] ⟩ | |
| /-! ## Main theorem -/ | |
| theorem 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 := by | |
| exact ⟨forward_direction lam, backward_direction lam⟩ | |
| end Submission |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Lean | |
| open Lean | |
| def comparatorExists (comparatorBin : String) : IO Bool := do | |
| if comparatorBin.contains '/' then | |
| return (← System.FilePath.pathExists comparatorBin) | |
| try | |
| let child ← IO.Process.spawn { | |
| cmd := "sh" | |
| args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin] | |
| } | |
| let exitCode ← child.wait | |
| return exitCode == 0 | |
| catch _ => | |
| return false | |
| def main : IO UInt32 := do | |
| let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator" | |
| if !(← comparatorExists comparatorBin) then | |
| IO.eprintln s!"Failed to run comparator via `{comparatorBin}`." | |
| IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`." | |
| IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export." | |
| pure 1 | |
| else | |
| try | |
| let child ← IO.Process.spawn { | |
| cmd := "lake" | |
| args := #["env", comparatorBin, "config.json"] | |
| } | |
| let exitCode ← child.wait | |
| pure exitCode | |
| catch err => | |
| IO.eprintln s!"Failed to run comparator via `{comparatorBin}`." | |
| IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`." | |
| IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export." | |
| IO.eprintln s!"Original error: {err}" | |
| pure 1 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment