I guess you got downvoted because it sounded like an ad.
But I think Lean Prover is a programming language with a lot of potential for AI alignment and is mentioned in Provably safe systems: the only path to controllable AGI. It would be good to have more knowledge about it on LessWrong.
I have written an essay “A Proposal for Safe and Hallucination-free Coding AI” (https://gasstationmanager.github.io/ai/2024/11/04/a-proposal.html), in which I propose an open-source collaboration on a research agenda that I believe will eventually lead to coding AIs that have superhuman-level ability, are hallucination-free, and safe.
Any Lean enthusiasts here? You might be interested to check out Code with Proofs: the Arena. Test your Lean skills with our coding challenges!
Code for the website is open sourced at https://github.com/GasStationManager/CodeProofTheArena
I guess you got downvoted because it sounded like an ad.
But I think Lean Prover is a programming language with a lot of potential for AI alignment and is mentioned in Provably safe systems: the only path to controllable AGI. It would be good to have more knowledge about it on LessWrong.
I have written an essay “A Proposal for Safe and Hallucination-free Coding AI” (https://gasstationmanager.github.io/ai/2024/11/04/a-proposal.html), in which I propose an open-source collaboration on a research agenda that I believe will eventually lead to coding AIs that have superhuman-level ability, are hallucination-free, and safe.
Comments are welcome!