Prof. Kontorovich, Informal Lecture on Mathematical Rigor and the Lean Theorem Prover

Discussion of the evolution of mathematical rigor over time, and potential future applications of Interactive Theorem Provers such as Microsoft's Lean.

[@RSLT]

I have seen this video many times, and I absolutely love it. Great Job, Alex!❤🧡💛👍👍👍👍

[@RSLT]

Fantastic lecture and very eye-opening. Do you think the limit definition is broken and needs to be fixed? 15:00 Quick note integral is a sum. The Symbol of integral "s" represents the Sum. dx is actually Δx. We know dx is not actually zero despite its definition x>0 lim x=0 . In other words, some people (last 100 years) get a bit superficial and ride too much on the limit definition. They turned it into a religion(culture) and a belief system rather than mathematical logic. 00:14, 2:39 Also, I believe some people are constantly in combat with complicated math problems and take that battle to the real world. People like Nobel relay dislike it, and the rest is bad blood that yet to be fixed. Every year some people celebrating science and not inviting the mathematicians. I'm trying to say 00:14, 2:39 not going to help math. They are scientists that do advance math as a day-to-day routine. Riemann's first paper was on electrical, and we know electrical engineers are ahead of mathematicians in complex analysis. Electrical engineers have invented devices that measure the electrical system's imaginary part!!

[@derschutz4737]

Terry Tao is one of the organizers of a workshop on machine theorem proving, are you attending next year?

[@thereGoMapo]

I like the idea, it can make math more accessible to amateurs and allow them to make contributions too! I don't like the syntax though, seems clumsy and undignified.

[@andreavaldroni7026]

Excellent

[@kdebcf6445]

If A^2 +B^2 = C^2 why : A+B+C= even number.

[@smolboye1878]

Do a case analysis with C even or odd

[@ronald3836]

By Fermat's little theorem (or simply by checking that 0^2 = 0 mod 2 and 1^2 = 1 mod 2), x^2 = x mod 2 for all integers x. Therefore, if A^2 + B^2 = C^2, we have A + B = A^2 + B^2 = C^2 = C mod 2. Thus A + B - C = 0 mod 2. SInce x = -x mod 2 for all x, this means A + B + C = 0 mod 2, i.e. A+B+C is even.

[@dopahar]

When did Greeks discover the modern decimal number system? Or when did they first use it? You suggest it was 300 BCE. Is that correct?