4 ms·
I think the proof assistants are getting very powerful, eg: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-de
by foxes 5y ago
I think the proof assistants are getting very powerful, eg:
https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
State of the art research explored with lean. I think a certain level of hand wavy romanticism is fine for a HN comment if it can inspire people to be interested in the field. I also would prefer to be corrected in a reasonable discussion than a silent chilling downvote.
- bmitc 5y agoThanks for the article/interview. I am intrigued to find Peter Scholze’s own words calling this a “human experience”. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/#comment-2299 https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... This is actually a great article that helps to show that humans are still very much involved in convincing each other, using machines to aid to that effect. Regarding downvotes, you can’t even downvote someone you’ve replied to or they’ve replied to you on Hacker News.