Skip to main content
7 votes

Kunen's inconsistency axiom-free proof on Metamath

The answer to this question is a tentative "yes", but it depends on how you interpret the resulting statement. From my understanding, there isn't anything about "elementary embedding&...
Mario Carneiro's user avatar
3 votes

Can Hyperreal exist a axiom-free implementation in HoTT?

For a survey of formalizations of real numbers you can look at Formalization of real analysis: a survey of proof assistants and libraries by Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. ...
Andrej Bauer's user avatar
  • 9,593

Only top scored, non community-wiki answers of a minimum length are eligible