#cslib — Public Fediverse posts

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

We offer a library-level solution in #CSLib through the 'HasFresh' typeclass. Whatever the type of x is, you just need to convince #Lean that there's a 'fresh' value generator and you're good to go with your proofs. For many types (like natural numbers), we've even already convinced Lean for you.

This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.

2/

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. https://arxiv.org/abs/2602.15078v1 #LeanProver #ITP #CSLib #CompSci

Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. https://arxiv.org/abs/2602.15409v1 #LeanProver #ITP #CSLib #CompSci

RE: https://mastodon.acm.org/@acp/115921453909423834

The recording for @fmontesi's Lean Together talk, "CSLib: The Lean Computer Science Library", is now online:

https://www.youtube.com/watch?v=KfIZn2zH8CA

#CSLib #LeanProver

@fmontesi is presenting the first results and next steps of CSLib – the Lean Computer Science library – at Lean Together tomorrow (20 Jan) at 14:00 CET. The event is online and open to all, so feel free to join if you're curious:

https://researchseminars.org/talk/LT2026/9/

@leanprover #CSLib #LeanProver

FORM (https://sdu.dk/form) is a new research centre at the University of Southern Denmark. It is a major investment in formalised computer science and reliable AI-assisted programming. We collaborate heavily with the #Lean FRO and other international partners on #CSLib.

~ Academic Positions in Formal Methods (postdoc, assistant prof., associate prof.) and Programming Languages (postdoc) ~

The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! Among other projects, FORM is also working on the formalisation of computer science as part of a global initiative, CSLib, in @leanprover.

(1/3)

#formalMethods #LeanProver #typeTheory #programmingLanguages #academicJobs #fediHire #FORMSDU #SDUDK #CSLib

@fmontesi will be the first director of the new Centre for Formal Methods and Future Computing (FORM) here at the University of Southern Denmark!

Among other things, the Centre will work on the development of @leanprover's CS Library, where Fabrizio already serves as a member of the steering committee.

Interested in research in formal methods? Please expect job announcements very soon.

https://sdu.dk/form

#formalMethods #LeanProver #CSLib #programmingLanguages #FORMSDU #SDUDK