Comme me l'a fait remarquer Patrick Massot, la ligne
Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !
# Petite rectification
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2.
Comme me l'a fait remarquer Patrick Massot, la ligne
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !