Yes absolutely too far: clickbait and that's unfortunate because it otherwise looks like a really well written article. It completely ignores all the work that happened in those 30 years before this Coq proof which only replicates (with more trustable steps) other work.