I have formalized an answer at Homeomorphisms and "mod finite" by @VilleSalo, in a moderately-sized Lean file.

Outcome: his claims turned out to be 100% accurate.

(The only stumbling block was that for me, it was easier to prove continuity of the inverse directly rather than appealing to general theory of compact and Hausdorff spaces.)

Has anyone verified other MathOverflow answers?

  • 2
    $\begingroup$ Nice! ${}{}{}{}$ $\endgroup$ Apr 24 at 0:01
  • 10
    $\begingroup$ Great! I would welcome the trend, if more people do this kind of thing. $\endgroup$ Apr 24 at 13:45
  • 2
    $\begingroup$ thank you for doing this! $\endgroup$ Apr 25 at 1:00

1 Answer 1


The #1 most popular question on MO is "Examples of common false beliefs in mathematics".

Here are verifications that these are indeed false beliefs. :)

Alternative link since that one may be down

  • $\begingroup$ (I wasn't able to do the #1 most popular answer because I don't know how to work with vector subspace dimension (submodule rank) in Lean.) $\endgroup$ May 6 at 1:06

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .