diff --git a/Leanwuzla/Parser.lean b/Leanwuzla/Parser.lean
index 57dddd0..604f1bf 100644
--- a/Leanwuzla/Parser.lean
+++ b/Leanwuzla/Parser.lean
@@ -1,5 +1,6 @@
 import Leanwuzla.Aux
 import Leanwuzla.Sexp
+import Fp
 
 open Lean
 
@@ -23,16 +24,44 @@ abbrev ParserM := StateT Parser.State (Except MessageData)
 namespace Parser
 
 private def mkBool : Expr :=
-  .const ``Bool []
+  toTypeExpr Bool
 
 private def mkBitVec (w : Nat) : Expr :=
-  .app (.const ``BitVec []) (mkNatLit w)
+  toTypeExpr (BitVec w)
+
+-- Temporary ToExpr instances for PackedFloat and RoundingMode
+deriving instance ToExpr for PackedFloat
+deriving instance ToExpr for RoundingMode
+
+private def mkFloat (eb sb : Nat) : Expr :=
+  toTypeExpr (PackedFloat eb sb)
+
+private def mkRoundingMode : Expr :=
+  toTypeExpr RoundingMode
+
+private def mkFloat16 : Expr :=
+  toTypeExpr (PackedFloat 5 (11 - 1))
+
+private def mkFloat32 : Expr :=
+  toTypeExpr (PackedFloat 8 (24 - 1))
+
+private def mkFloat64 : Expr :=
+  toTypeExpr (PackedFloat 11 (53 - 1))
+
+private def mkFloat128 : Expr :=
+  toTypeExpr (PackedFloat 15 (113 - 1))
 
 private def getBitVecWidth (α : Expr) : ParserM Nat := do
   match α with
   | .app (.const ``BitVec []) w => return w.nat?.get!
   | _ => throw m!"Error: expected BitVec type, got {α}"
 
+private def getFloatEbSb (α : Expr) : ParserM (Nat × Nat) := do
+  match α with
+  | .app (.app (.const ``PackedFloat []) eb) sb =>
+    return (eb.nat?.get!, sb.nat?.get!)
+  | _ => throw m!"Error: expected PackedFloat type, got {α}"
+
 private def mkInstBEqBool : Expr :=
   mkApp2 (.const ``instBEqOfDecidableEq [0]) mkBool
          (.const ``instDecidableEqBool [])
@@ -125,6 +154,20 @@ def parseSort (s  : Sexp) : ParserM (Expr × Expr) := do
   | sexp!{(_ BitVec {w})} =>
     let w := w.serialize.toNat!
     return (mkBitVec w, mkBitVec w)
+  | sexp!{(_ FloatingPoint {eb} {sb})} =>
+    let eb := eb.serialize.toNat!
+    let sb := sb.serialize.toNat!
+    return (mkFloat eb (sb - 1), mkFloat eb (sb - 1))
+  | sexp!{Float16} =>
+    return (mkFloat16, mkFloat16)
+  | sexp!{Float32} =>
+    return (mkFloat32, mkFloat32)
+  | sexp!{Float64} =>
+    return (mkFloat64, mkFloat64)
+  | sexp!{Float128} =>
+    return (mkFloat128, mkFloat128)
+  | sexp!{RoundingMode} =>
+    return (mkRoundingMode, mkRoundingMode)
   | sexp!{({sc} ⦃as⦄)} =>
     let (bsc, sc) ← parseSort sc
     let as ← as.mapM parseSort
@@ -159,9 +202,9 @@ where
       let e := bindings.foldr (fun (n, t, v) b => .letE n t v b true) b
       return (tb, e)
     if let sexp!{true} := e then
-      return (mkBool, .const ``true [])
+      return (mkBool, toExpr true)
     if let sexp!{false} := e then
-      return (mkBool, .const ``false [])
+      return (mkBool, toExpr false)
     if let sexp!{(not {p})} := e then
       let (_, p) ← parseTerm p
       return (mkBool, .app (.const ``not []) p)
@@ -178,10 +221,11 @@ where
     if let sexp!{(= {x} {y})} := e then
       let (uα, x) ← parseTerm x
       let (_, y) ← parseTerm y
-      let hα ← if uα == mkBool then pure mkInstBEqBool
-        else if uα.isAppOfArity ``BitVec 1 then pure (mkInstBEqBitVec (← getBitVecWidth uα))
+      let beqOp ← if uα == mkBool then pure (mkApp2 (.const ``BEq.beq [0]) uα mkInstBEqBool)
+        else if uα.isAppOfArity ``BitVec 1 then pure (mkApp2 (.const ``BEq.beq [0]) uα (mkInstBEqBitVec (← getBitVecWidth uα)))
+        else if uα.isAppOfArity ``PackedFloat 2 then let (eb, sb) ← getFloatEbSb uα; pure (mkApp2 (.const ``PackedFloat.smtBeq []) (toExpr eb) (toExpr sb))
         else throw m!"Error: unsupported type for equality: {uα}"
-      return (mkBool, mkApp4 (.const ``BEq.beq [0]) uα hα x y)
+      return (mkBool, mkApp2 beqOp x y)
     if let sexp!{(distinct ⦃xs⦄)} := e then
       return ← pairwiseDistinct xs
     if let sexp!{(ite {c} {t} {e})} := e then
@@ -351,6 +395,178 @@ where
       let (α, x) ← parseTerm x
       let w ← getBitVecWidth α
       return (α, mkApp3 (.const ``BitVec.rotateRight []) (mkNatLit w) x (mkNatLit i))
+    if let sexp!{roundNearestTiesToEven} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RNE)
+    if let sexp!{RNE} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RNE)
+    if let sexp!{roundNearestTiesToAway} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RNA)
+    if let sexp!{RNA} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RNA)
+    if let sexp!{roundTowardPositive} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTP)
+    if let sexp!{RTP} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTP)
+    if let sexp!{roundTowardNegative} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTN)
+    if let sexp!{RTN} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTN)
+    if let sexp!{roundTowardZero} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTZ)
+    if let sexp!{RTZ} := e then
+      return (mkRoundingMode, toExpr RoundingMode.RTZ)
+    if let sexp!{(fp {sign} {ex} {sig})} := e then
+      let some ⟨1, sign⟩ := parseBVLiteral? sign | throw m!"Error: expected sign to be a bit-vector literal"
+      let some ⟨eb, ex⟩ := parseBVLiteral? ex | throw m!"Error: expected exponent to be a bit-vector literal"
+      let some ⟨sb, sig⟩ := parseBVLiteral? sig | throw m!"Error: expected significand to be a bit-vector literal"
+      return (mkFloat eb sb, toExpr (PackedFloat.mk sign.msb ex sig))
+    if let sexp!{(_ +oo {eb} {sb})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      return (mkFloat eb sb, toExpr (PackedFloat.getInfinity eb sb false))
+    if let sexp!{(_ -oo {eb} {sb})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      return (mkFloat eb sb, toExpr (PackedFloat.getInfinity eb sb true))
+    if let sexp!{(_ +zero {eb} {sb})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      return (mkFloat eb sb, toExpr (PackedFloat.getZero eb sb false))
+    if let sexp!{(_ -zero {eb} {sb})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      return (mkFloat eb sb, toExpr (PackedFloat.getZero eb sb true))
+    if let sexp!{(_ NaN {eb} {sb})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      return (mkFloat eb sb, toExpr (PackedFloat.getNaN eb sb))
+    if let sexp!{(fp.abs {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp3 (.const ``PackedFloat.abs []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.neg {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp3 (.const ``PackedFloat.neg []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.add {rm} {x} {y})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp5 (.const ``PackedFloat.add []) (mkNatLit eb) (mkNatLit sb) rm x y)
+    if let sexp!{(fp.sub {rm} {x} {y})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp5 (.const ``PackedFloat.sub []) (mkNatLit eb) (mkNatLit sb) rm x y)
+    if let sexp!{(fp.mul {rm} {x} {y})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp5 (.const ``PackedFloat.mul []) (mkNatLit eb) (mkNatLit sb) rm x y)
+    if let sexp!{(fp.div {rm} {x} {y})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp5 (.const ``PackedFloat.div []) (mkNatLit eb) (mkNatLit sb) rm x y)
+    if let sexp!{(fp.fma {rm} {x} {y} {z})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (_, z) ← parseTerm z
+      let (eb, sb) ← getFloatEbSb α
+      return (α, mkApp6 (.const ``PackedFloat.fma []) (mkNatLit eb) (mkNatLit sb) rm x y z)
+    if let sexp!{(fp.sqrt {rm} {x})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      -- return (α, mkApp4 (.const ``sqrt []) (mkNatLit eb) (mkNatLit sb) x rm)
+      throw m!"Error: `fp.sqrt` is not supported, yet"
+    if let sexp!{(fp.rem {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      -- return (α, mkApp4 (.const ``remainder []) (mkNatLit eb) (mkNatLit sb) x y)
+      throw m!"Error: `fp.rem` is not supported, yet"
+    if let sexp!{(fp.roundToIntegral {rm} {x})} := e then
+      let (_, rm) ← parseTerm rm
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      -- return (α, mkApp4 (.const ``roundToInt []) (mkNatLit eb) (mkNatLit sb) rm x)
+      throw m!"Error: `fp.roundToIntegral` is not supported, yet"
+    if let sexp!{(fp.min {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      -- return (α, mkApp4 (.const ``flt_min []) (mkNatLit eb) (mkNatLit sb) x y)
+      throw m!"Error: `fp.min` is not supported, yet"
+    if let sexp!{(fp.max {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      -- return (α, mkApp4 (.const ``flt_max []) (mkNatLit eb) (mkNatLit sb) x y)
+      throw m!"Error: `fp.max` is not supported, yet"
+    if let sexp!{(fp.leq {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp4 (.const ``PackedFloat.smtBle []) (mkNatLit eb) (mkNatLit sb) x y)
+    if let sexp!{(fp.lt {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp4 (.const ``PackedFloat.smtBlt []) (mkNatLit eb) (mkNatLit sb) x y)
+    if let sexp!{(fp.geq {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp4 (.const ``PackedFloat.smtBge []) (mkNatLit eb) (mkNatLit sb) x y)
+    if let sexp!{(fp.gt {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp4 (.const ``PackedFloat.smtBgt []) (mkNatLit eb) (mkNatLit sb) x y)
+    if let sexp!{(fp.eq {x} {y})} := e then
+      let (α, x) ← parseTerm x
+      let (_, y) ← parseTerm y
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp4 (.const ``PackedFloat.ieeeBeq []) (mkNatLit eb) (mkNatLit sb) x y)
+    if let sexp!{(fp.isNormal {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.isNorm []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isSubnormal {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.isSubnorm []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isZero {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.isZero []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isInfinite {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.isInfinite []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isNaN {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.isNaN []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isNegative {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.smtIsNeg []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{(fp.isPositive {x})} := e then
+      let (α, x) ← parseTerm x
+      let (eb, sb) ← getFloatEbSb α
+      return (mkBool, mkApp3 (.const ``PackedFloat.smtIsPos []) (mkNatLit eb) (mkNatLit sb) x)
+    if let sexp!{((_ to_fp {eb} {sb}) {x})} := e then
+      let eb := eb.serialize.toNat!
+      let sb := sb.serialize.toNat! - 1
+      let (β, x) ← parseTerm x
+      return (mkFloat eb sb, mkApp3 (.const ``PackedFloat.ofBits []) (mkNatLit eb) (mkNatLit sb) x)
     if let some r ← parseVar? e then
       return r
     if let some ⟨w, x⟩ := parseBVLiteral? s then
@@ -412,19 +628,20 @@ where
     else
       let (α, as0) ← parseTerm as[0]
       let (_, as1) ← parseTerm as[1]
-      let hα ← if α == mkBool
-        then pure mkInstBEqBool
-        else if α.isAppOfArity ``BitVec 1 then pure (mkInstBEqBitVec (← getBitVecWidth α))
+      let bneOp ← if α == mkBool
+        then pure (mkApp2 (.const ``bne [0]) α mkInstBEqBool)
+        else if α.isAppOfArity ``BitVec 1 then pure (mkApp2 (.const ``bne [0]) α (mkInstBEqBitVec (← getBitVecWidth α)))
+        else if α.isAppOfArity ``PackedFloat 2 then let (eb, sb) ← getFloatEbSb α; pure (mkApp2 (.const ``PackedFloat.smtBne []) (toExpr eb) (toExpr sb))
         else throw m!"Error: unsupported type for `distinct`: {α}"
-      let mut acc : Expr := mkApp4 (.const ``bne [0]) α hα as0 as1
+      let mut acc : Expr := mkApp2 bneOp as0 as1
       for hi : i in [2:as.length] do
         let (_, asi) ← parseTerm as[i]
-        acc := mkApp2 (.const ``and []) acc (mkApp4 (.const ``bne [0]) α hα as0 asi)
+        acc := mkApp2 (.const ``and []) acc (mkApp2 bneOp as0 asi)
       for hi : i in [1:as.length] do
         for hj : j in [i + 1:as.length] do
           let (_, asi) ← parseTerm as[i]
           let (_, asj) ← parseTerm as[j]
-          acc :=  mkApp2 (.const ``and []) acc (mkApp4 (.const ``bne [0]) α hα asi asj)
+          acc :=  mkApp2 (.const ``and []) acc (mkApp2 bneOp asi asj)
       return (mkBool, acc)
   parseNestedBindings (bindings : List (List Sexp)) : ParserM (List (Name × Expr × Expr)) := do
     let bindings ← bindings.mapM parseParallelBindings
diff --git a/Main.lean b/Main.lean
index 4b7e0b8..c55c7d8 100644
--- a/Main.lean
+++ b/Main.lean
@@ -131,7 +131,7 @@ unsafe def runLeanwuzlaCmd (p : Parsed) : IO UInt32 := do
   let context := argsToContext p
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
-  let env ← importModules #[`Std.Tactic.BVDecide, `Leanwuzla.Aux] {} 0 (loadExts := true)
+  let env ← importModules #[`Std.Tactic.BVDecide, `Leanwuzla.Aux, `Fp] {} 0 (loadExts := true)
   let coreContext := { fileName := "leanwuzla", fileMap := default, options }
   let coreState := { env }
   let code ← SolverM.run parseAndDecideSmt2File context coreContext coreState
diff --git a/lake-manifest.json b/lake-manifest.json
index 00023c3..ac2209c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/lean4-cli",
+ [{"url": "https://github.com/opencompl/fp-lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f047d3ec1bcbbfe23a1dfcd40c33794b38c7da97",
+   "name": "«fp-lean»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
@@ -10,6 +20,86 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
    "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4-nightly-testing",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b4b270b6d806fc808ee66f4c5fa8e79e7ece49ad",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing-2026-01-14",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ca46151b876597b20728bd65794928efda180d13",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "368243f6a97d18db0d5a2a8568aa44e261496ef7",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "25b1494bbf3663d3418ef81918af8ec3b000cf54",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "652cdcba9ee81b4d621b8a10315d48f8ae05bca8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.83-pre2",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2a6ce7931d891ab9a2a9e6260d281d5659040a7b",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0a83ad726ee0236e9574ef48098beedca30aa5a0",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c7df72751d64f426ce8e36b9f20f99c00ced0db2",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "leanwuzla",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 5fcfe03..9fa8adf 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,3 +18,8 @@ supportInterpreter = true
 scope = "leanprover"
 name = "Cli"
 rev = "nightly-testing"
+
+[[require]]
+git = "https://github.com/opencompl/fp-lean"
+name = "fp-lean"
+rev = "main"
diff --git a/lean-toolchain b/lean-toolchain
index 26e10ff..c0e7fa6 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-05
+leanprover/lean4:nightly-2026-01-14
\ No newline at end of file