This week, we made an experiment teaching proof and proving to high-school students(15yo) using Frédéric Tran Minh's Yalep, a layer above Lean.
Julien Narboux
@jnarboux
- 120 Followers
- 149 Following
- 52 Posts
Computer Science Researcher, Formal proof, geometry, computer science unplugged, les décodeuses d'informatique
@TaliaRinger you can use GeoCoq as an underlying library for a list of statements , we should discuss collaborations.
@KyC il va se passer la même chose pour l’education.
KyC« Je ne protège que les maisons qui sont sur ma liste. C’est ça la différence entre moi et les pompiers de l’État. Eux vont protéger chaque maison. Moi je ne protège que les maisons qui sont inscrites dans notre programme »
https://mrmondialisation.org/los-angeles-en-feu-triste-spectacle-des-inegalites/
Los Angeles en feu : triste spectacle des inégalités
Impossible de rester de marbre devant les images du méga-feu ayant ravagé Los Angeles. Mais au-delà de la catastrophe, les informations qui nous parviennent suscitent certaines réflexions et la récupération politique des puissants créent énormément de confusion, allant jusqu'à effacer les causes systémiques d'un tel drame. Essayons de voir clair ensemble. Édito. Comme beaucoup, on
Thomas SeillerYesterday, I gave a talk entitled “Does language have a logical structure?”.
I discussed a very recent collaboration with S. Jarvis and John Terilla (CUNY), G. Gastaldi @giannigastaldi, and L. Pellissier @lucpellissier.
I am quite excited about this work which relates categorical structures (nuclei of an adjunction), models of linear logic, and some approaches in natural language processing, with hints of projective tropical geometry.
Slides are here: https://www.seiller.org/Normes24.pdf
⏚ Antoine Chambert-LoirMarine Le Pen condamnée en appel pour diffamation envers La Cimade @lacimade
Toute personne éprise de liberté et de justice ne pourra que s'en féliciter. Et manifester sa gratitude pour l'action de cette association, fondées par des chrétiens protestants il y a près de 100 ans, dont l'action pendant la seconde guerre mondiale a permis de sauver de nombreux Juifs, et qui œuvre chaque jour en faveur des personnes opprimées, exploitées, réfugiées, migrantes…
Le tome 2 du Tangente Éducation sur l’informatique débranchée est sorti. #infosansordi #csunplugged
@Dominique74230 je sais pas en effet les slides ne donnent pas la réf du papier.
Quand les collègues de science de l’éducation te présentent la meta analyse qui montre que les trois mesures Attal (redoublement, uniforme, groupes niveaux) sont les pires idées qu’on puisse avoir.
