Comment by infruset

> "Georges Gonthier, a computer scientist at Inria in Paris"

somehow the article forgets to mention he was the guy who came up with the first Coq (now Rocq) formal proof of the Four Color Theorem..