3 ms·
This is also a part of why I am somewhat fascinated by the idea and the state of Lean4 and mathlib in Lean4. People put more and more formally verified proofs i
by tetha 3y ago
This is also a part of why I am somewhat fascinated by the idea and the state of Lean4 and mathlib in Lean4. People put more and more formally verified proofs into mathlib, which in turn makes formally proving further theorems in mathlib easier.
If you start with nothing (like in the numbers game), simple proofs are a lot of ... just effort, because you have specify a lot of rewrites and overall work. In mathlib, however, systems like simp (the simplification system) or linarith ("There is a solution by linear arithmetic") seem to do a lot of heavy, repetitive lifting by now.
It's a really interesting snowball effect. Sadly, everything I understand is most likely already in there, so I doubt I could contribute meaningfully, haha.
- IanCal 3y agoThat's very interesting, I'm no mathematician but I should have a play around with it. > Sadly, everything I understand is most likely already in there, so I doubt I could contribute meaningfully, haha. I wouldn't be so sure - and even if so then remember there's enormous benefit to improving tooling around a system. If you want to be involved somehow, better devx, tutorials, output, packaging, error messages all make a big difference to end users. Edit - As another thought, is there benefit in going through papers and translating that work into lean4? I'm not really familiar enough with it but if so that may 1. Find issues in current work, like Tao did in his own work 2. Add to a reusable body of work
- lmpdev 3y agoFormer computational mathematics major You absolutely can contribute meaningfully The maths world is incomprehensibly broad and deep, even if you just take the Erdos approach and go for interesting but shallow problems