The Future of Mathematics?

What Hacker News said

Recommends stephenSinniah · 2019-10 · on “Learning How to Prove: From the Coq Proof Assistant to Textbook Style”

I was watching a video by Kevin Buzzard, he talks about using Lean Theorem Prover, seems pretty interesting [this video]

Recommends infogulch · 2019-10 · on “Alloy is a language for describing structures and a tool for exploring them”

Last week Microsoft Research posted an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with theorem provers. He's currently using LEAN [2]. Half of the talk is a discussion of the challenges he's faced convincing other mathematicians that this is valuable, and the other half is about his success using LEAN as a tool to teach undergraduates about formal proofs in general. I think Alloy was mentioned at the end, but not really compared to LEAN. [1]: [this video] [2]: [LINK]

Recommends Nzen · 2019-10 · on “A Code Glitch May Have Caused Errors in More Than a Hundred Published Studies”

For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN. He highlights cultural misunderstanding and apathy on both sides of the domain divide. He also references the idea that the people who might make the appropriate tools may not have stayed in academia. So, he's structured his courses around using LEAN with the indirect consequence that power users (undergrads) may choose to become open source committers. [0] [this video] One hour of presentation and then 15 min of q/a. My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some a

Recommends carapace · 2020-11 · on “Building the Mathematical Library of the Future”

Oh man that was fun! Totally nerd-sniped my day though. Got me to go back and re-watch Kevin Buzzard's talk at MS Research in re: Lean, "The Future of Mathematics?" [this video] [LINK]

Recommends andrewnc · 2021-05 · on “Z3 Tutorial”

That was a delightful tutorial, I recently watched a talk about the Future of Mathematics[0] with respect to theorem proving and formalization. I enjoy this area a lot and love to see it getting more attention. 0 - [this video]

Recommends oolonthegreat · 2021-07 · on “Some stuff I found interesting about number theory research”

wanted to drop a link to buzzard's very interesting talk [this video] starting at 13:00 he talks about that frailness. also loved the bit about "elders" at 40:37

Recommends liups · 2021-12 · on “The year in math and computer science”

> pure math (topology and countability) and computer science have almost no overlap in the short term. This is an unexpected opinion. What do you mean by this? I would argue the opposite. Look at Formal Verification[0]. Here's a great video about a popular formal verfication proof assitant: [this video] A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek) Formal Verification would see

Recommends pas · 2023-10 · on “Lean4 helped Terence Tao discover a small bug in his recent paper”

Kevin Buzzard (a professional mathematician) has a few good talks about Lean [this video] from 2019 at MS Research [LINK] (2022 at ICM international math congress)