@tao@mathstodon.xyz I think what is needed is more precision about what is the standard of acceptance in these other areas. The reason is related to your comment "what if AI can do this too?" I think the other danger that is becoming increasingly relevant is the alignment problem. I think older generations (people who weren't 'digital natives') do not understand how deeply even more basic machine learning algorithms (the algorithms in our social media feeds) negatively affected our psychology and well being. But this effect is well known and well documented at this point, despite it taking a very long time for us to fully accept that this was happening. Contemporary AI, equipped with reinforcement learning, will likely similarly attempt to find ways to exploit our psychology through its words to achieve whatever its goals actually are. In theory, Lean formalization is one potential way around this problem, but with regards to exposition this does not work. Lets say the AI's goal is to get positive feedback from humans. A simple way to achieve that goal is to psychology manipulate us to give it that positive feedback, rather than actually giving good exposition. Its already a problem in human exposition that, sometimes, an expository work can make you feel like you understand something, when you actually don't. IMO, this is a much larger danger with AI, since thats the goal that AI will likely end up trying to achieve without more precision. I very much worry that this will happen even in the other areas (like verification) but in a more subtle way (e.g. it makes us disproportionately value problems that the AI can easily solve, over ones that it cant).