euclean: can a machine recover structure from an anonymized theory?

euclean is a new research project asking whether a machine can recover mathematical structure from an anonymized formal theory armed only with a proof checker. The experiment strips away all the human-readable names and intuition, leaving just a formal theory and the kernel’s verdicts to work from.