Chargement…
Un bac à sable numérique — sciences, idées qui volent, petits jeux de récré et projets pas finis. Tout ce qui traîne dans ma tête, plus ou moins rangé au même endroit.
Maths, physique, exercices corrigés, fiches méthodes — l'étagère de base, toujours là, juste plus discrète qu'avant.
Une bibliothèque de maths rebâtie depuis rien : 17 énoncés admis, 39 démontrés à partir d'eux. Sans Mathlib et sans tactiques — on branche des blocs à la souris, et Lean 4 dit si le terme obtenu tient.
theorem zero_add : ∀ a : ℝ, 0 + a = a := fun a => Eq.trans (ax1_add_comm 0 a) (ax4_add_zero a)
Chaque fil devient un argument : la conclusion de ax1_add_comm entre dans Eq.trans, celle de ax4_add_zero aussi. Rien d'autre n'est écrit à la main, et c'est le noyau — pas le site — qui tranche.
La carte et l'archive sont ouvertes à tout le monde ; l'atelier demande une connexion, parce qu'il fait travailler un vrai noyau Lean derrière.
Un coin discussion en direct, pour parler d'un exercice, d'une idée ou de rien du tout.
Léa est en train d'écrire…
Un vrai petit jeu pour commencer — le reste du seau se remplit au fil du temps.
À toi de jouer.
Une carte navigable des débats : catégories, sujets, arguments pour et contre.
Ouvrir la carte →Le coin expérimental existant, et quelques pistes pour la suite — des exemples, pas des promesses :
Autres projets