Sign in Create account

#lean3 — Public Fediverse posts

Live and recent posts from across the Fediverse tagged #lean3, aggregated by home.social.

José A. Alonso @[email protected] · 2024-09-22 · 09:15 UTC

Readings shared September 21, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/21-readings_shared_09-21-24 #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning

#deeplearning #llms #ai #math #logic #mathlib
José A. Alonso @[email protected] · 2024-09-07 · 09:56 UTC

Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. https://docta.ucm.es/rest/api/core/bitstreams/d40e94d0-be70-4df1-88bc-6461f3a905ed/content #ITP #Maude #LeanProver #Lean3

#lean3 #leanprover #maude #itp
Askar Safin @[email protected] · 2023-08-15 · 17:58 UTC

It seems one can represent ZFC (or any other logic or type system) as Lean 3's GADT. Note that binder very elegantly represented as HOAS. Am I first who discovered this? #types.pl #plt #lean #lean3 #gadt #zfc #hoas
https://lobste.rs/s/11k4ri/how_should_i_read_type_system_notation#c_rtpme5

#types #plt #lean #lean3 #gadt #zfc