Hacker News
- Formalising modern research mathematics in real time https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ 16 comments
- Beyond the Liquid Tensor Experiment https://xenaproject.wordpress.com/2022/09/12/beyond-the-liquid-tensor-experiment/ 10 comments
- The future of interactive theorem proving? https://xenaproject.wordpress.com/2022/08/16/the-future-of-interactive-theorem-proving/ 16 comments
- Formalising Mathematics: An Introduction https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/ 116 comments
- A mathematical formalisation challenge by Peter Scholze https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ 24 comments
- Division by zero in type theory: a FAQ https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ 82 comments
- Mathematics in type theory https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ 22 comments
- Where is the fashionable mathematics? https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ 64 comments
- A computer-generated proof that nobody understands – Xena https://xenaproject.wordpress.com/2019/07/06/a-computer-generated-proof-that-nobody-understands/ 2 comments
Lobsters
- Half a year of the Liquid Tensor Experiment: Amazing developments https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ 2 comments formalmethods , math
- Division by zero in type theory: a FAQ https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ 3 comments math , plt
- Does anyone “know” a proof of Fermat’s Last Theorem? https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ 12 comments math
- Lean in 2024 | Kevin Buzzard's blog post https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ 10 comments math
- Beyond the Liquid Tensor Experiment, "the formalisation of a proof of a complex theorem about complex objects ... Johan Commelin, assisted by Adam Topaz and a team of other mathematicians, announced earlier this month that their Lean formalisation of Scholze’s challenge was complete." https://xenaproject.wordpress.com/2022/09/12/beyond-the-liquid-tensor-experiment/ 10 comments math
- The Future of Interactive Theorem Proving? "Lean Chat, a VS-code extension that provides an interface for autoformalizing natural language theorem statements in Lean. Under the hood, these translation are generated by OpenAI’s Codex, a text generation model trained on Github source code." https://xenaproject.wordpress.com/2022/08/16/the-future-of-interactive-theorem-proving/ 17 comments math
- Half a year of the Liquid Tensor Experiment: Amazing developments https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ 28 comments math
- Formalising mathematics: an introduction. https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/ 37 comments math
- Peter Scholze has written a guest post for Xena project, posing a challenge to formalize a proof and explaining the background and his interest in it https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ 33 comments math
- Rigorous mathematics: "What is rigorous mathematics? It means mathematics which is guaranteed to be correct. It is mathematics which has been checked from the axioms, perhaps because it has been read so many times ... But not all of our human [mathematics] literature is rigorous mathematics." https://xenaproject.wordpress.com/2019/12/07/rigorous-mathematics/ 8 comments math
- [computer-assisted proof] PhD students have used Lean to prove that a normed real vector space with compact unit ball is finite-dimensional https://xenaproject.wordpress.com/2019/12/07/prove-a-theorem-write-a-function/ 10 comments math
- Counting binary relations: an apology https://xenaproject.wordpress.com/2019/10/26/counting-binary-relations-an-apology/ 7 comments math
- On the Xena Project blog: Abhimanyu Pallavi Sudhir, a current first year, has used the Lean theorem prover to formalise the solutions to last year's final exam for Imperial College's "Introduction to Proofs" course https://xenaproject.wordpress.com/2019/05/06/m1f-imperial-undergraduates-and-lean/ 3 comments math
- The Xena Project: "I would like to see the main definitions, theorems and proofs, and example sheet questions and solutions, in all of the undergraduate pure mathematics courses at Imperial College London, typed up into formal proof verification software." https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/ 15 comments math