ForMatUS: Ejercicios con Lean sobre aritmética real

En el vídeo se comentan distintas pruebas con Lean de ejercicios sobre la aritmética de los números reales. La primera es por reescritura, la segunda es con encadenamiento de ecuaciones y las restantes son automáticas.

Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.

A continuación, se muestra el vídeo