Announcement_46

I experimented a bit with Claude-generated Lean formalizations. It managed to formalize a proof of Lovász’s theorem (two graphs are isomorphic if, and only if, they are homomorphism indistinguishable over all graphs) and of some of the result from Logical equivalences, homomorphism indistinguishability, and forbidden minors. Check out the repository.