Our Projects

• Buchberger’s Algorithm in Lean 4
  Formalization of Gröbner bases and Buchberger’s criterion using Mathlib in Lean 4.

• Faugère’s F4 Algorithm
  Formalization in Lean 4 and certified verification of Faugère’s F4 algorithm for Gröbner basis computation.

• Autoformalization in Lean
  Developing tools for translating informal mathematical statements into Lean.