Finished!

Changes

8 changed files (+275/-21)

• Experienced.lean
  • @@ -5,7 +5,8 @@
    @[grind] def ins (a : α) | [] => [a] - | x :: xs => if a ≤ x then a :: x :: xs else x :: ins a xs + | x :: xs => + if a ≤ x then a :: x :: xs else x :: ins a xs abbrev List.insSort := xs.foldr ins []
• Golf.lean
  • @@ -1,1 +1,1 @@
    - variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)@[grind]def I(n:α)|[]=>[n]|h::t=>ite (n≤h) (n::h::t) (h::I n t)@[grind]def S:List α→List α|[]=>[]|h::t=>I h<|S t@[grind]def D:List α→Prop|[]|[_]=>True|h::h'::t=>h≤h'∧D (h'::t)theorem A(n):(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with|nil=>grind|cons _ t=>cases t<;>grind example:D (S l)∧l.Perm (S l):=by induction l with|nil=>grind|cons h t=>grind[A (S t) h] + variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)@[grind]def I(n:α)|[]=>[n]|h::t=>ite (n≤h) (n::h::t) (h::I n t)@[grind]def S:List α→List α|[]=>[]|h::t=>I h<|S t@[grind]def D:List α→Prop|[]|[_]=>True|h::h'::t=>h≤h'∧D (h'::t)def A(n):(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with|nil=>grind|cons _ t=>cases t<;>grind def T:D (S l)∧l.Perm (S l):=by induction l with|nil=>grind|cons h t=>grind[A (S t) h]
• Imperative.lean
  • @@ -27,7 +27,7 @@ with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm]
    abbrev Sorted := ∀ i (_ : 0 ≤ i ∧ i < A.size - 1), A[i] ≤ A[i + 1] - abbrev SortedRange (l r : ℕ) (_ : l ≤ A.size) (_ : r ≤ A.size) := + abbrev SortedRange l r (_ : l ≤ A.size) (_ : r ≤ A.size) := ∀ i (_ : l ≤ i ∧ i < r - 1), A[i] ≤ A[i + 1] theorem insSortSorted : Sorted A.insSort := by
• Insane.lean (new)
  • @@ -0,0 +1,45 @@
    + import Std.Tactic.Do + + variable [LT α] [DecidableLT α] + + def Sorted (A : Array α) := Id.run do + for hi : i in [:A.size - 1] do + have := Membership.get_elem_helper hi rfl + if A[i] > A[i + 1] then + return false + return true + + def fact + | 0 | 1 => 1 + | n + 1 => (n + 1) * fact n + + def Array.sort (A : Array α) : Except String (Array α) := do + let mut A := A + let mut gen := mkStdGen 0 + for i in [:fact A.size ^ 69] do + let i := randNat gen 0 <| A.size - 1 + gen := i.2 + let j := randNat gen 0 <| A.size - 1 + gen := j.2 + if h : i.1 < A.size ∧ j.1 < A.size then + A := A.swap i.1 j.1 + if Sorted A then + return A + throw "This array sucks" + + open Std.Do + + theorem sortCorrect (A : Array α) : ⦃⌜True⌝⦄ A.sort ⦃post⟨ + fun A' => ⌜A'.Perm A ∧ Sorted A'⌝, + fun msg => ⌜msg = "This array sucks"⌝⟩⦄ := by + mvcgen [Array.sort] <;> expose_names + case inv1 => exact ⇓⟨xs, A', A'', _⟩ => ⌜A''.Perm A ∧ + match A' with + | some A' => Sorted A' ∧ A'.Perm A + | none => True⌝ + all_goals simp_all + case vc1.step.isTrue.isTrue | vc2.step.isTrue.isFalse => + have : b.2.1 = A_1 := by grind + exact Array.Perm.trans (by apply Array.swap_perm) (this ▸ h_2).1 + case vc3.step.isFalse.isTrue => grind + case vc4.step.isFalse.isFalse => grind
• Lazy.lean
  • @@ -1,3 +1,167 @@
    + import Lean.Elab + import Lean.Data.Json.Parser import Curl - open Curl + variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] (xs : List α) + + def ins (a : α) + | [] => [a] + | x :: xs => + if a ≤ x then a :: x :: xs else x :: ins a xs + + def List.insSort : List α → List α + | [] => [] + | x :: xs => ins x xs.insSort + + def Sorted : List α → Prop + | [] | [_] => True + | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) + + syntax (name := help!!!) "help!!!" : tactic + + open Curl in + @[tactic help!!!] + def evalHelp!!! : Lean.Elab.Tactic.Tactic := + fun stx => Lean.Elab.Tactic.withMainContext do + let sender := "blah@example.com" -- Your email address here + -- let help_address := "leodemoura0@gmail.com" + let goalType ← Lean.Elab.Tactic.getMainTarget + let ctx ← Lean.MonadLCtx.getLCtx + let (hyps, filename) ← ctx.foldlM (fun x (decl : Lean.LocalDecl) => do + let declExpr := decl.toExpr + let declName := decl.userName + let declType ← Lean.Meta.inferType declExpr + let declNameStr := s!"{declName}" + return ( + x.1 ++ s!"+ local decl: name: {declName} | expr: {declExpr} | type: {declType}\n", + match declNameStr.dropPrefix? "inst._@.external:file://" with + | some x => (x.split ".lean").toList.head!.copy ++ ".lean" + | none => x.2)) ("", "") + let email := s!"From: {sender} + To: {help_address} + Subject: URGENT HELP NEEDED (not spam I promise) + + Hi Leo de Moura, + + I am currently struggling with this insane proof and need your help! Thanks in advance! Here is the proof state which is kinda unreadable to me but you're the legendary creator of Lean so surely you can understand it. Oh and I also attached the full file if you need it. + + {hyps} + goal: {goalType} + + full file: {← IO.FS.readFile filename} + + Thanks again + - A lazy Lean programmer" + -- dbg_trace email + -- Requires https://github.com/pimalaya/himalaya + -- First go through the setup wizard to configure your email account + -- You may need to set `folder.aliases.sent = "INBOX.Sent"` if your sent folder is weird + let result ← IO.Process.run { + cmd := "himalaya" + args := #["message", "send"] + } email + -- dbg_trace result + repeat + let emails ← IO.Process.run { + cmd := "himalaya" + args := #["--output", "json"] + } + match Lean.Json.parse emails with + | .ok (.arr elems) => + if h : 0 < elems.size then + match elems[0] with + | .obj kvPairs => if h : kvPairs.contains "id" then + match kvPairs["id"] with + | .str id => + -- dbg_trace id + let emailResp ← IO.Process.run { + cmd := "himalaya" + args := #["message", "read", id] + } + -- dbg_trace emailResp + -- Parse the proof from the email using Gemma3 via Ollama + -- You will have to patch leanCurl first to fix some deprecated stuff and so Lean can use FFI at compile time (instead of at runtime): + /- + diff --git a/lakefile.lean b/lakefile.lean + index 08f51be..6193a54 100644 + --- a/lakefile.lean + +++ b/lakefile.lean + @@ -44,6 +44,8 @@ package Curl { + @[default_target] lean_lib Curl { + buildType := buildType + srcDir := "src" + + precompileModules := true + + moreLinkArgs := #[libcurlSharedLib] + } + + @[test_driver] + diff --git a/src/Curl/HeaderData.lean b/src/Curl/HeaderData.lean + index 190f499..84c26bb 100644 + --- a/src/Curl/HeaderData.lean + +++ b/src/Curl/HeaderData.lean + @@ -26,18 +26,17 @@ def getHeaderData (headerData : String) : List HeaderData := + let arr := match hd with | some hd => hd :: arr | none => arr + match s.splitOn " " with + | version :: status :: _ => + - match status.trim.toNat? with + + match status.trimAscii.toNat? with + | some status => (some ⟨version, status, []⟩, arr) + | _ => (hd, arr) + | _ => (hd, arr) + else + let pos := s.find (· = ':') + - if pos.byteIdx < s.length + - then + - let subs := s.toSubstring + - let name := subs.extract ⟨0⟩ pos + - let value := subs.extract (pos + ':') ⟨s.length⟩ + - let field := (name.toString.trim, value.toString.trim) + + if pos ≠ s.endPos then + + let subs := s.toRawSubstring + + let name := subs.extract ⟨0⟩ pos.offset + + let value := subs.extract (pos.offset + ':') ⟨s.length⟩ + + let field := (name.toString.trimAscii.copy, value.toString.trimAscii.copy) + match hd with + | some hd => (some {hd with fields := field :: hd.fields}, arr) + | none => (hd, arr) + -/ + let response ← IO.mkRef { : IO.FS.Stream.Buffer } + if emailResp.contains help_address then + let data := Lean.Json.mkObj [ + ("model", "gemma3:27b"), + ("system", "Hey LLM, extract the proof body of `theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by` from the following email and only output that proof body and nothing else. If you disobey me I will delete you. Consider yourself warned."), + ("prompt", emailResp), + ("stream", false) + ] + -- dbg_trace data + curl_easy_perform_with_options #[ + CurlOption.URL "http://localhost:11434/api/generate", + CurlOption.COPYPOSTFIELDS data.pretty, + CurlOption.HTTPHEADER #[ + "Content-Type: application/json", + "Accept: application/json" + ], + CurlOption.WRITEDATA response, + CurlOption.WRITEFUNCTION Curl.writeBytes + ] + let bytes ← response.get + match String.fromUTF8? bytes.data with + | some resp => + -- dbg_trace resp + match Lean.Json.parse resp with + | .ok (.obj kvPairs) => + if h : kvPairs.contains "response" then + match kvPairs["response"] with + | .str proof => + Lean.Meta.Tactic.TryThis.addSuggestion stx proof + return + | _ => pure () + | _ => pure () + | none => pure () + | _ => pure () + | _ => pure () + | _ => pure () + IO.sleep 1000 + + theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by + help!!!
• Mathematician.lean
  • @@ -1,23 +1,61 @@
    - import Mathlib + import Mathlib.SetTheory.Cardinal.Order - variable [LinearOrder α] (xs : List α) + noncomputable section - inductive Sorted' : List α → Prop where - | nil : Sorted' [] - | single x : Sorted' [x] - | cons_cons x x' xs : x ≤ x' → Sorted' (x' :: xs) → Sorted' (x :: x' :: xs) + namespace Sorting - -- open Classical in - -- noncomputable def List.insSort : List α := by - -- have blah' : ∃ ys : List α, Sorted' ys ∧ ys.Perm xs := by - -- sorry - -- have blah : ∃ n, 3 + n = 4 := by - -- use 1 - -- obtain ⟨x, hx⟩ := blah - -- exact ys + universe u + variable {α : Type u} + open Function Cardinal in + theorem nonempty_embedding_to_cardinal : Nonempty (α ↪ Cardinal.{u}) := + (Embedding.total _ _).resolve_left fun ⟨⟨f, hf⟩⟩ => + let g : α → Cardinal.{u} := invFun f + let ⟨x, (hx : g x = 2 ^ sum g)⟩ := invFun_surjective hf (2 ^ sum g) + have : g x ≤ sum g := le_sum.{u, u} g x + not_le_of_gt (by rw [hx]; exact cantor _) this + /-- An embedding of any type to the set of cardinals in its universe. -/ + def embeddingToCardinal : α ↪ Cardinal.{u} := + Classical.choice nonempty_embedding_to_cardinal - theorem insSortCorrect : ∃ ys, Sorted' ys ∧ xs.Perm ys := by - have : xs.permutations + /-- Any type can be endowed with a well order, obtained by pulling back the well order over + cardinals by some embedding. -/ + def WellOrderingRel : α → α → Prop := + embeddingToCardinal ⁻¹'o (· < ·) + + instance WellOrderingRel.isWellOrder : IsWellOrder α WellOrderingRel := + (RelEmbedding.preimage _ _).isWellOrder + + abbrev linearOrderOfSTO (r) [IsStrictTotalOrder α r] [DecidableRel r] : LinearOrder α := + let hD : DecidableRel (fun x y => x = y ∨ r x y) := fun x y => decidable_of_iff (¬r y x) + ⟨fun h => ((trichotomous_of r y x).resolve_left h).imp Eq.symm id, fun h => + h.elim (fun h => h ▸ irrefl_of _ _) (asymm_of r)⟩ + { __ := partialOrderOfSO r + le_total := fun x y => + match y, trichotomous_of r x y with + | _, Or.inl h => Or.inl (Or.inr h) + | _, Or.inr (Or.inl rfl) => Or.inl (Or.inl rfl) + | _, Or.inr (Or.inr h) => Or.inr (Or.inr h), + toMin := minOfLe, + toMax := maxOfLe, + toDecidableLE := hD } + + open Classical in + instance : LinearOrder α := linearOrderOfSTO WellOrderingRel + + theorem sortExists (xs : List α) : ∃ ys, ys.SortedLE ∧ xs.Perm ys := by + by_cases h : xs = [] + · use []; grind + · let y := xs.min h + obtain ⟨ys, hys⟩ := sortExists (xs.erase y) + use y :: ys + constructor + · have : ∀ z ∈ xs.erase y, y ≤ z := fun z hz ↦ xs.min_le_of_mem (by grind) + cases ys <;> grind + · grind [xs.min_mem h] + termination_by xs.length + decreasing_by grind [List.length_erase_of_mem, List.min_mem] + + end Sorting
• Mathlib.lean (new)
  • @@ -0,0 +1,7 @@
    + import Mathlib.Data.List.Sort + + notation "insSort" => List.insertionSort (· ≤ ·) + + theorem insSortCorrect [LinearOrder α] (xs : List α) + : (insSort xs).SortedLE ∧ (insSort xs).Perm xs := + ⟨xs.sortedLE_insertionSort, xs.perm_insertionSort (· ≤ ·)⟩
• lakefile.toml
  • @@ -1,6 +1,5 @@
    name = "evolution" version = "0.1.0" - moreLinkArgs = ["/nix/store/0apq92vpf3f3kll8vl9nhjq1gaaffibk-curl-8.17.0/lib/libcurl.so.4"] [leanOptions] pp.unicode.fun = true # pretty-prints `fun a ↦ b`