On Thursday, July 2, 2020 at 6:48:08 AM UTC-5 Philip Thrift wrote: > https://arxiv.org/abs/2007.00418 > > [Submitted on 1 Jul 2020] > *Forcing as a computational process* > > > Something in a real language (Lean 3):
*A formalization of forcing and the unprovability of the continuum hypothesis [in Lean]* https://arxiv.org/abs/1904.10570 authors: https://jesse-michael-han.github.io/ http://florisvandoorn.com/ https://github.com/jesse-michael-han/flypitch https://flypitch.github.io/ *The Flypitch project aimed to produce a formal proof of the independence of the continuum hypothesis.* *We have completed our original objective. We are now refining our library and exploring other formalization projects related to forcing and mathematical logic.* Our formalization uses *Lean*, an open source theorem prover and programming language primarily developed by Leonardo de Moura at Microsoft Research. @philipthrift -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/b0c101a1-65b8-49fb-823f-a356a87b019cn%40googlegroups.com.
