For mathematical monologue, dialogue, discourse, in short for communication including proofs ("A proof is any completely convincing argument"
[Errett Bishop: "Schizophrenia in contemporary mathematics", Amer. Math. Soc. Colloquium Lecture, Seventy-eighth summer meeting, University of Montana, Missoula, Montana (1973)]), every language is suitable. This includes abstract logic-based languages as well as ordinary spoken language like German, English, Latin, geometrical drawings and even gestures. The snooty Bourbaki-attitude admitting only a very narrow spectrum of languages may be welcomed by those who have problems with other languages. But with respect to the failure of this approach to recognize the fatal mistakes of modern set theory (see for instance https://philosophy.stackexchange.com/questions/51038/will-mcduck-go-bankrupt) this language cannot be recommended, and "machine checked proof" is not a mark of quality.
"Pure mathematics and science are finally being reunited and, mercifully, the Bourbaki plague is dying out." [Murray Gell-Mann: "Nature conformable to herself", Bulletin of the Santa Fe Institute 7 (1992) p. 7]
Of course a rigorous geometrical proof is as correct as any other. For people with corresponding sensual perception it is even better.