SeQLean: Verifying SQL queries using Lean

We present \emph{SeQLean}, a system that uses formal verification in Lean to increase the accuracy of translation from natural language to SQL. This is based on modelling SQL in Lean via relational algebras. Since we do not have a translation known to be correct, we cannot directly prove correctness. Instead, we use \emph{proof challenges}: tests of internal consistency that are unlikely to be satisfied by an incorrect translation. The simplest proof challenge is based on generating two translations of the same natural language query into SQL, ideally with one being optimized for performance and the other for understandability. If two translations are equivalent, they must give the same answer for every database. This can be checked using proof automation in Lean. Using Lean allows us to have essentially arbitrary properties as proof challenges, and also check these (including equivalence) taking into account known properties of the underlying database system. Even for equivalence queries of an arithmetic nature, we show that Lean can be more powerful than traditional tools due to the availability of Mathlib theorems. A JSON API over HTTP allows the verifier to be integrated into agentic frameworks.