Junyan Xu

icon indicating an email [email protected]

icon location Heidelberg / Shenzhen icon location PhD in Math, working on Lean's mathlib4 and formalization of FLT. Interested in autoformalization and AI for mathematics.

Results 181 comments of Junyan Xu

feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets

I've formalized your suggested proof of `#ZFSet=univ` [here](https://github.com/leanprover-community/mathlib4/commit/28032d06ce3ca5158f90e840986b8126b9393352), but it increases transitive imports from 531 to 640 due to Cardinal.Arithmetic. Would you include it in this PR? And can you...