Lean

Publication d'une preuve formelle en Lean et d'un article affirmant résoudre l'un des sept problèmes du millénaire.

Des chercheurs rapportent que l'IA les a aidés à découvrir A-greement, un protocole de consensus pour machines à états géo-répliquées qui réduit la latence moyenne face aux meilleures solutions existantes.

Basis montre que des LLMs peuvent rédiger la sémantique formelle d'un petit langage, puis prouver sous Lean que son interpréteur la respecte, jusqu'au code RISC-V compilé.

Une méthode combine revue sémantique par LLM et contrôles mécaniques numériques et de vacuité pour vérifier des formalisations Lean et repérer des erreurs que les LLM juges laissent passer.

Terence Tao examine la fiabilité de l'assistant de preuve Lean et le rôle croissant de l'IA dans la formalisation mathématique, à l'intention des mathématiciens.

La page Science d'Anthropic présente son équipe, ses collaborations avec universités et biotechs, et ses travaux récents : carte UV du ciel, preuve de Fermat en Lean, conception de protéines.

Des chercheurs formalisent en Lean une preuve mathématique assistée par IA du problème de packing optimal de 11 carrés dans un carré unitaire.

Une étude théorique établit à quelles conditions un langage infini inconnu peut être appris à partir d'exemples positifs, avec preuves formalisées en Lean.

OpenAI publie une solution générée par IA à l'un des sept problèmes du millénaire, avec preuve formelle en Lean.

Les chercheurs utilisent un assistant d'IA pour formaliser la preuve du grand théorème de Fermat en Lean.

Un nouveau benchmark évalue si les agents IA peuvent produire, à l'échelle d'un dépôt entier, du code et des preuves formelles cohérents.