Can One Rule Tell You Everything About a Strange Operation?
An equation may hide consequences—or admit a counterexample. Meet a proof-search system that checks both paths and reveals where its search stalls.
equational reasoning
When Equations Resist Proof, Build a World Where They Fail
A new solver tackles abstract algebra from both sides: deriving consequences or constructing counterexamples, then asking Lean to verify every answer.