Sostactic es una herramienta innovadora que extiende las capacidades de los sistemas de demostración de teoremas como Lean 4 para probar desigualdades polinómicas. Tradicionalmente, probar estas desigualdades en Lean ha sido limitado por tácticas como nlinarith y positivity. Sostactic supera estas limitaciones al aprovechar una combinación de Lean 4 y un backend en Python que utiliza técnicas de descomposición de suma de cuadrados (SOS).
¿Cómo funciona? Sostactic se basa en el principio de descomposición SOS, una técnica matemática que permite expresar un polinomio como una suma de cuadrados de otros polinomios. El backend en Python, impulsado por el solucionador de optimización convexa cvxpy, encuentra estas descomposiciones SOS. Debido a que la solución de la programación semidefinida (SDP) involucrada es numérica, Sostactic emplea técnicas de racionalización y proyección para obtener una solución exacta, que luego se verifica dentro de Lean. Esto es crucial porque las soluciones numéricas pueden ser imprecisas y no siempre conducen a una demostración formal.
Aplicaciones: Sostactic es útil en una variedad de contextos, incluyendo:
* Demostración de no negatividad global: Probar que un polinomio es siempre no negativo, independientemente de los valores de sus variables.
* Demostración de no negatividad en conjuntos semialgebraicos: Probar que un polinomio es no negativo dentro de un conjunto definido por un sistema de desigualdades polinómicas. Esto es útil para demostrar propiedades de regiones geométricas.
* Prueba de la imposibilidad: Demostrar que un sistema de desigualdades polinómicas no tiene solución, lo que implica que un conjunto definido por esas desigualdades está vacío.
Ejemplos concretos: El repositorio incluye ejemplos que ilustran su uso, como la demostración de la desigualdad AM-GM, la desigualdad de Motzkin y la demostración de que ciertos conjuntos de discos son disjuntos, casos en los que tácticas más simples fallan. También permite demostrar la no negatividad de un polinomio en un intervalo específico, como 4x³ - 3x + 1 ≥ 0 en el intervalo [0, 1].
Consideraciones: Sostactic no es una solución mágica. La conversión de la solución numérica a una demostración exacta puede fallar debido a problemas de precisión numérica. En estos casos, el sistema proporciona sugerencias para ayudar al usuario a ajustar la solución, como aumentar el grado de la descomposición o usar plantillas explícitas. Además, requiere Python 3.10+ y la instalación de dependencias específicas, incluyendo cvxpy y sympy. Es importante mantener la versión de Mathlib sincronizada con la versión utilizada por Sostactic para evitar incompatibilidades.