Kim Morrison

I'm happy to announce the release of further packages for Hex, the computer algebra library for Lean, following lattice basis reduction, certified integer polynomial factorization and certified graph isomorphism.

I'm very excited to release HexGraphIso, a new sublibrary of Hex, which implements (a subset of) Brendan McKay's nauty in Lean, proves it correct, and provides a tactic layer.

It's been a month since we launched, so I'd like to make a brief post highlighting some of the results that have landed in Tau Ceti.

Today we're launching the Palomar Registry, an index of formalized mathematics repositories with a valid #comparator setup and #formalization.yaml metadata.

I'm happy to announce the release of further packages for Hex, the computer algebra library for Lean.

I can't possibly be serious, can I, claiming that Lean is faster than Rust?

We're starting work on a computational algebra library for Lean, called Hex.

I've released leanprover/lp: verified linear programming in Lean 4.

I've put together an sos tactic: a sum-of-squares decision procedure for nonlinear real arithmetic, closely following John Harrison's implementation in HOL Light.