Our team—Samuel Korda, Bhanu Jangam, Nicole Medeiros, Muhammad Yusuf, and Vignon Oussa—is currently completing a full Lean formalization of two important, well-established results related to the HRT Conjecture. Further details will be released at the end of the project.
