Create accountLogin

Recent searches

No recent searches

Search options

Not available on lingo.lol.
lingo.lol is one of the many independent Mastodon servers you can use to participate in the fediverse.
A place for linguists, philologists, and other lovers of languages.

Administered by:

Server stats:

60
active users

lingo.lol: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.8

#leanprover

21 posts7 participants3 posts today
Public
José A. Alonso

Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco et als. arxiv.org/abs/2505.19975v1 #ITP #LeanProver #Math

arXiv logo
arXiv.orgFormalizing a classification theorem for low-dimensional solvable Lie algebras in LeanWe present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such ubiquitous in geometry and physics. Our work involves explicit calculations on the level of the underlying vector spaces and provides a use case for the linear algebra and Lie theory routines in Lean's mathematical library mathlib. Along the way we formalize results about Lie algebras, define the semidirect product within this setting and add API for bases of vector spaces. In a wider context, this project aims to provide a complete mechanization of a classification theorem, covering both the statement and its full formal proof, and contribute to the development and broader adoption of such results in formalized mathematics.
Public
José A. Alonso

VERINA: Benchmarking verifiable code generation. ~ Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song. arxiv.org/abs/2505.23135 #AIforCode #ITP #LeanProver

arXiv logo
arXiv.orgVERINA: Benchmarking Verifiable Code GenerationLarge language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often lack support for end-to-end verifiable code generation. In this paper, we introduce Verina (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. Verina consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o4-mini, generates only 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task. We hope Verina will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.
Public
José A. Alonso

Formalizing colimits in Cat. ~ Mario Carneiro, Emily Riehl. arxiv.org/abs/2503.20704 #ITP #LeanProver

arXiv logo
arXiv.orgFormalizing colimits in CatCertain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite $\infty$-category theory has not been formalized. To support future work on formalizing $\infty$-category theory in Lean's mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that $\mathcal{C}\textsf{at}$ has colimits. To our knowledge this is the first formalized proof that the category of categories is cocomplete.
ExploreLive feeds
About