11 ms·
Surprised you didnt go into something AI adjacent
by brcmthrowaway 2y ago
Surprised you didnt go into something AI adjacent
- adamnemecek 2y agoLean is AI adjacent.
- saagarjha 2y agoOnly because the AI people find it interesting. It's not really AI in itself.
- cwzwarich 2y agoIf you’re interested in applications of AI to mathematics, you’re faced with the problem of what to do when the ratio of plausible proofs to humans that can check them radically changes. There are definitely some in the AI world who feel that the existing highly social construct of informal mathematical proof will remain intact, just with humans replaced by agents, but amongst mathematicians there is a growing realization that formalization is the best way to deal with this epistemological crisis. It helps that work done in Lean (on Mathlib and other developments) is reaching an inflection point just as these questions become practically relevant from AI.
- mkl 2y agoIt's not AI in itself, but it's one of the best possibilities for enabling AI systems to generate mathematical proofs that can be automatically verified to be correct, which is needed at the scale they can potentially operate. Of course it has many non-AI uses too.
- ofrzeta 2y agoThey do have AI on their roadmap, though: https://lean-fro.org/about/roadmap-y2/ https://lean-fro.org/about/roadmap-y2/
- fspeech 2y agoIf you want to have superhuman performance like AlphaZero series you need a verifier (valuation network) to tell you if you are on the right track. Lean (proof checker) in general can act as a trusted critic.
- zozbot234 2y agoProof automation definitely counts as AI. Not all AI is based on machine learning or statistical methods, GOFAI is a thing too.
- trenchgun 2y agoIt's not ML, but it is AI
- fantod 2y agoI don't know what his reasons are but it makes sense to me. Yes, there are incredible results coming out of the AI world but the methods aren't necessarily that interesting (i.e. intellectually stimulating) and it can be frustrating working in a field with this much noise.
- uoaei 2y agoI don't want to come across as too harsh but having studied machine learning since 2015 I find the most recent crop of people excited about working on AI are deep in Dunning-Kruger. I think I conflate this a bit with the fascination of results over process (I suppose that befuddlement is what led me to physics over engineering) but working in ML research for so long it's hard to gin up a perspective that these things are actually teleologically useful, and not just randomly good enough most of the time to keep up the illusion.
- croemer 2y agoWhat do you mean by "things that are actually teleologically useful"? Fellow physicist here by the way
- Baeocystin 2y agoNot OP, but I'm assuming he means that they are maddeningly black-boxy, if you want to know how the sausage is made.
- uoaei 2y agoLike useful in an intentional way: purpose-built and achieves success via accurate, parsimonious models. The telos here being the stated goal of a structurally sound agent that can emulate a human being, as opposed to the accidental, max-entropy implementations we have today.
- calf 2y agoIs a guide dog teleologically useful?
- oulipo 2y agoThis is *VERY* AI-adjacent... the next batch of AI algos will need to integrate reasoning through theorem provers to go next level