#### Welcome to Science4All

My name is Lê and I believe that the greatest challenge in education is to make science and math appealing.

This is why I aim at bringing enthusiasm and excitement to the readers’ learning experience.

I now run a Robustly Beneficial wiki, mostly on AI ethics, which has come to fascinate me!

Type Theory: A Modern Computable Paradigm for Math Type Theory: A Modern Computable Paradigm for Math

By Lê Nguyên Hoang |

In 2013, three dozens of today's brightest minds have just laid out new foundation of mathematics after a year of collective effort. This new paradigm better fits both informal and computationally-checkable mathematics. There is little doubt that it will fundamentally change our perspective on rigorous knowledge, and it could be that, in a few decades, the book they published turns out to be the bedrock of all mathematics, and, by extension, all human knowledge! Have a primer of this upcoming revolution, with this article on type theory, the theory that the book builds upon!

By Lê Nguyên Hoang |

**Updated:**2016-01 |**Views**: 11186In 2013, three dozens of today's brightest minds have just laid out new foundation of mathematics after a year of collective effort. This new paradigm better fits both informal and computationally-checkable mathematics. There is little doubt that it will fundamentally change our perspective on rigorous knowledge, and it could be that, in a few decades, the book they published turns out to be the bedrock of all mathematics, and, by extension, all human knowledge! Have a primer of this upcoming revolution, with this article on type theory, the theory that the book builds upon!