Noah Weninger

Stream: new members

[Noah Weninger]

Hi everyone! I'm an MSc student at UBC (Vancouver, Canada) studying theoretical computing science--specifically approximation algorithms for knapsack problems. I've become very interested in using Lean in my research after watching Kevin Buzzard's talk "The Future of Mathematics?". Given that I'm still learning Lean, It's not looking likely at this point that I'll be able to both produce novel results in my thesis and formally verify it. However, for my PhD (which I'm currently looking for supervisors for), I am now rather committed to my plan of formalizing it. To me, it just seems so incredibly natural to have computers check and aid with proofs, particularly in TCS, where one would hope that people are already sold on the value of computers! So it's been very surprising that I've only found a few people who are formally verifying approximation algorithms and that I've only found classical results. I wonder if anyone can shed light on this. Also, please tell me if I'm crazy for wanting to formalize my whole thesis :smile:

[Jasmin Blanchette]

Some topics benefit more from formalization than others. Sometimes, formalizing as you go is more efficient than working on paper -- that's what the programming language community is finding, and also the term-rewriting community. My gut feeling is that a hybrid approach might be best: that you formalize some of your results but not all. Otherwise formalization might slow you down too much.