“The Examples Are Indeed Extremely Simple on Purpose (otherwise It’s Hard to Communicate Efficiently What’s Happening to Non-Metamath Experts). That Being Said, We’re Still Pretty Far Away from IMOs; but This Is Definitely a Goal for Us, and One We’re Actively Working Towards!”, Stanislas Polu (, , )

The Examples Are Indeed Extremely Simple on Purpose (otherwise It’s Hard to Communicate Efficiently What’s Happening to Non-Metamath Experts). That Being Said, We’re Still Pretty Far Away from IMOs; but This Is Definitely a Goal for Us, and One We’re Actively Working Towards!