This repository contains some experimental code aimed at solving arithmetic problems in Lean 4.

It currently consists of a normalization routine that maps arithmetic predicates and terms into a normal form so that the solver has fewer special cases to addresss.