Formalizing the Auslander-Buchsbaum-Serre Theorem
The Auslander-Buchsbaum-Serre theorem is a key result in commutative algebra that characterizes when a Noetherian local ring is regular in terms of global dimension.
I’m formalizing a proof of this theorem in Lean as a contribution to Mathlib. This involves encoding key concepts like depth, homological dimension, and properties of local rings to build toward a fully verified proof. The goal is to make this result accessible within Lean’s ecosystem for use in other algebraic formalization efforts.
We hope to publish our work sometime this year.
Formalizing Grammar-Constrained Decoding
Grammar-constrained decoding ensures that large language models (LLMs) generate outputs that follow strict syntactic rules. The algorithm in this paper provides a flexible and efficient way to enforce these constraints during decoding.
I’m working on a Lean formalization of this algorithm with the UCSD Programming Systems Group to rigorously verify its correctness. This will help ensure reliability in structured text generation tasks like code synthesis and theorem proving, with potential applications in proof automation and verified AI systems.