The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

50 years of proof assistants. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html #ITP #IsabelleHOL #CoqProver #HOL

50 years of proof assistants. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html #ITP #IsabelleHOL #CoqProver #HOL

Conjecture extraction for proof autoformalization. ~ Simon Sorg, Wenda Li, Soumya Banerjee. https://www.researchgate.net/profile/Soumya_Banerjee/publication/396932859_Conjecture_extraction_for_proof_autoformalization/links/68ff6c60a404d657099f1f89/Conjecture-extraction-for-proof-autoformalization.pdf #AI #Math #ITP #LeanProver #Autoformalization

Conjecture extraction for proof autoformalization. ~ Simon Sorg, Wenda Li, Soumya Banerjee. https://www.researchgate.net/profile/Soumya_Banerjee/publication/396932859_Conjecture_extraction_for_proof_autoformalization/links/68ff6c60a404d657099f1f89/Conjecture-extraction-for-proof-autoformalization.pdf #AI #Math #ITP #LeanProver #Autoformalization

È stato molto bello aver potuto partecipare ieri sera, sia pure da remoto, all’Italian Teacher Programme “Galileo”. È stato bello essere stati chiamati a parlare di ciò che più mi sta a cuore, adesso. L'accoglienza è stata calda e amichevole, a valle del mio intervento si è sviluppato un bel dialogo. Ricorderò sempre la serata di ieri con affetto. E spero la prossima volta di essere lì di persona!

https://edu.inaf.it/news/per-la-scuola/italian-teacher-programme-galileo-canarie-2025/

#eventi #itp #letteratura #scienza #divulgazione

È stato molto bello aver potuto partecipare ieri sera, sia pure da remoto, all’Italian Teacher Programme “Galileo”. È stato bello essere stati chiamati a parlare di ciò che più mi sta a cuore, adesso. L'accoglienza è stata calda e amichevole, a valle del mio intervento si è sviluppato un bel dialogo. Ricorderò sempre la serata di ieri con affetto. E spero la prossima volta di essere lì di persona!

https://edu.inaf.it/news/per-la-scuola/italian-teacher-programme-galileo-canarie-2025/

#eventi #itp #letteratura #scienza #divulgazione

Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. https://openreview.net/forum?id=OM7ZN0PmSS #LLMs#ITP#LeanProver#Math

Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. https://openreview.net/forum?id=OM7ZN0PmSS #LLMs#ITP#LeanProver#Math

Kacie Kinzer’s Tweenbots are small cardboard robots that roam the city helped by strangers. They have many wabi-sabi qualities and I make the case that empathy is one of them.
https://wabitronics.com/examples/tweenbots/

#wabisabi #electronics #robotics #itp #moma #empathy

Kacie Kinzer’s Tweenbots are small cardboard robots that roam the city helped by strangers. They have many wabi-sabi qualities and I make the case that empathy is one of them.
https://wabitronics.com/examples/tweenbots/

#wabisabi #electronics #robotics #itp #moma #empathy