Formalización del algoritmo de división multivariada en Lean 4

Abstract

Lean es un asistente de demostración interactivo y un lenguaje de programación funcional muy expresivo, que permite formalizar y verificar demostraciones matemáticas, y construir herramientas para interactuar con estas en un mismo entorno. En este trabajo, presentamos el Cálculo de las Construcciones Inductivas sobre el que se fundamenta la axiomática de Lean, introduciremos brevemente algunas de las capacidades del lenguaje que serán de utilidad, e introduciremos Mathlib, un esfuerzo colectivo por formalizar las matemáticas contemporáneas en Lean. Finalmente, presentaremos una formalización propia del algoritmo de división multivariada en Lean 4, junto con una prueba de su corrección.

Lean is an interactive theorem prover and a very expressive functional programming language, which can be used to formalize and verify mathematical proofs and build tools to interact with these in a single environment. In this document, we present the Calculus of Inductive Constructions on which Lean’s axiomatic foundation is based, we briefly present some of the language’s capabilities of interest, and introduce Mathlib, a collective effort to formalize contemporary mathematics in Lean. Finally, we present our own formalization of the multivariate division algorithm in Lean 4, along with a proof of its correctness.