Lean 4 interface to Eigen
Proof of concept for interfacing Eigen’s linear solvers in Lean 4.
To compile and build examples:
lake script run compileCpp
lake build
lake scropt run buildExamples
Example of solving simple 2x2 system with LDLT:
def main : IO Unit := do
let A : Matrix 2 2 := ⟨FloatArray.mk #[2,1,1,2], by native_decide⟩
let b : Matrix 2 1 := ⟨FloatArray.mk #[1,1], by native_decide⟩
IO.println A
IO.println b
IO.println (A.ldlt.solve b)
To run the example ./build/exmaples/dense
.
Example of initializing sparse matrix:
def main : IO Unit := do
let entries : Array (Triplet 2 2) := (#[(0,0,1.0), (1,1,-1.0), (0,1, 2.0)] : Array (Nat×Nat×Float))
let B := SparseMatrix.mk entries
IO.println B.toDense
To run the example ./build/exmaples/sparse
.