# Author Archives: xenaproject

## Lean Together 2021

A discussion of some of the talks from the Lean Together conference. Continue reading

## The end of the summer.

It’s the end of the summer now, so it must finally be time to talk about the summer projects, and the things which happened since then. Continue reading

## Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge. Continue reading

## Thoughts on the Pythagorean theorem

Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading

## Two types of universe for two types of mathematician

Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits I see I have done just enough to … Continue reading

## Lean for the Curious Mathematician 2020

Lean for the Curious Mathematician 2020 just happened. It was interesting. Continue reading

## Division by zero in type theory: a FAQ

How can a theorem prover use the convention that 1/0=0 and still be consistent? Continue reading

## Equality, specifications, and implementations

There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on Continue reading

## Teaching dependent type theory to 4 year olds via mathematics

What is the number before 0? Who cares! How do children model numbers? An experiment with type theory. Continue reading

## Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms Continue reading