4 ms·

I think the art is moved from the proof itself to translating the proof to computer language. Edit: typo