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.
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.