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

Edit: typo