Výzkumná organizace Millennium Research vydala open-source nástroj leanscreen, který kontroluje, jestli formální matematické věty v systému Lean 4 skutečně tvrdí to, co tvrdit mají. Často se stává, že důkaz projde kompilátorem, ale tvrzení je ve skutečnosti prázdné, například dokazuje triviální rovnost místo slíbeného výsledku. Nástroj umí rychlé linty, kontrolu vakuit a elaboraci proti knihovně mathlib, i hlubší kontrolu se dvěma nezávislými soudci a zkouškou proti-příkladu. Autoři nástroj kalibrovali na 886 lidských posudcích. Nástroj je zdarma, běží lokálně a jednotlivou kontrolu zvládne zhruba za desetinu sekundy. Podle autorů má pomoci hlavně při ověřování výsledků generovaných AI modely.
