{"id":"palomar/PALOMAR-2026-09-01-000007","url":"https://github.com/Arthur742Ramos/equality-saturation-checker-lean/tree/e74222fe2591b15837d1bc239b58a14170d4bccc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000007-v1.json","repo":"https://github.com/Arthur742Ramos/equality-saturation-checker-lean","tags":["cs.LO","cs.PL","math.LO","msc:03B35","msc:68Q42","formal-verification","e-graphs","lean","program-optimization"],"score":0,"title":"Native Lean equality-saturation certificate checking","trust":"high","domain":"cs.LO","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"cs.LO","summary":"Formalizes a native Lean checker for certified finite acyclic e-graphs. The principal result proves that accepted class certificates connect a canonical e-class term to the executable extracted representative and establish its minimum additive cost among all represented terms. The development also covers chronological merge certificates, egg-style flat explanations, replay-backed extraction, and bounded certificate search.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"Checking Equality-Saturation Merge and Extraction Certificates","identifier":"https://isa-afp.org/entries/Equality_Saturation_Checker.html","relationship":"adapts"}]}