Univalent Foundation – Computer Proof of All Maths

The scary complex field of Math worried the mathematicians who would prove a theorem relying on the previous theorems assumed proven correct by other mathematicians.

A sad example was Zhang YiTang (1955 – ) who prepared his PhD Thesis based on a previous “flawed” Theorem proved by none other than his PhD Advisor Prof Mok in Purdue University. Unfortunately his Thesis was found wrong, and the tragic happened to Zhang as he had revealed the mistake of his PhD advisor who insisted his (Mok’s) Theorem was correct. As a result Zhang failed the 7-year PhD course without any teaching job recommendation letter from his angry advisor. He ended with a Subway Sandwich Kitchen job offered by his Chinese friend, sleeping in another Chinese music conductor’s house on a sofa. It was there he spent another 7 years thinking on Math, finally an Eureka breakthrough one 2013 morning in the backyard wild forest – the proof of the famous “70 million Prime Gap Conjecture”!

Univalent Foundation was born out of the same requirement by the (late) mathematician Vladimir Voevodsky (1966 – 2017) [#] – Use computer to prove Mathematics !


Note : [#] Vladimir Voevodsky


One thought on “Univalent Foundation – Computer Proof of All Maths

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s