Created
May 2, 2026 12:00
-
-
Save kim-em/2666a4ee006d01d8353fec4ea5282eda to your computer and use it in GitHub Desktop.
lean-eval Aristotle (Harmonic) submission for exists_nonisotopic_link
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 ChallengeDeps | |
| open LeanEval.KnotTheory | |
| theorem exists_nonisotopic_link : ∃ L₁ L₂ : TwoLink, ¬ L₁.Isotopic L₂ := 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": [ | |
| "exists_nonisotopic_link" | |
| ], | |
| "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 = "exists_nonisotopic_link" | |
| 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 = "ChallengeDeps" | |
| [[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 ChallengeDeps | |
| import Submission | |
| open LeanEval.KnotTheory | |
| theorem exists_nonisotopic_link : ∃ L₁ L₂ : TwoLink, ¬ L₁.Isotopic L₂ := by | |
| exact Submission.exists_nonisotopic_link |
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 ChallengeDeps | |
| open LeanEval.KnotTheory | |
| namespace Submission | |
| theorem exists_nonisotopic_link : ∃ L₁ L₂ : TwoLink, ¬ L₁.Isotopic L₂ := by | |
| exact ⟨.unlink, .hopfLink, by decide⟩ | |
| 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