Xena

Mathematicians learning Lean by doing.

Skip to content

Home
About Xena
Student projects
What maths is in Lean?
Installing Lean and mathlib
Twitter
Useful links.

Tag Archives: computability

Proofs are not programs

Posted on June 15, 2019 by xenaproject

A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading →

Posted in computability | Tagged axiom of choice, bytecode, computability, Curry-Howard | 5 Comments

The inverse of a bijection.

Posted on June 11, 2019 by xenaproject

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading →

Posted in Learning Lean, M1F | Tagged computability, M1F | 10 Comments

Search for:
Categories

Recent Posts
- Lean in 2024 January 20, 2024
- Formalising modern research mathematics in real time November 4, 2023
- Lean 2022 round-up January 8, 2023
- Beyond the Liquid Tensor Experiment September 12, 2022
- The Future of Interactive Theorem Proving? August 16, 2022

Create a free website or blog at WordPress.com.

Privacy & Cookies: This site uses cookies. By continuing to use this website, you agree to their use.
To find out more, including how to control cookies, see here: Cookie Policy

Subscribe Subscribed
- Xena
- Already have a WordPress.com account? Log in now.