Skip to content

Instantly share code, notes, and snippets.


Andrej Bauer andrejbauer

View GitHub Profile
View beamer-slides-with-notes.pdf
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
andrejbauer / UniverseInjection.agda
Last active Oct 11, 2020
Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.
View UniverseInjection.agda
-- Counterexample by Chung Kil Hur, improved by Andrej Bauer
-- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle.
-- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set),
-- which by Lawvere's fixed point theorem begets a fixed point operator on Set.
-- However, negation does not have a fixed point.
module cantor where
-- generalities
andrejbauer / ConstructibleNumbers.nb
Last active Sep 25, 2020
Generation of constructible numbers in Mathematica
View ConstructibleNumbers.nb
(* Content-type: application/vnd.wolfram.mathematica *)
(*** Wolfram Notebook File ***)
(* *)
(* CreatedBy='Mathematica 11.2' *)
(*CacheID: 234*)
(* Internal cache information:
andrejbauer / mandelbrot.c
Created Dec 11, 2013
A simple program for computing the Mandelbrot set.
View mandelbrot.c
This program is an adaptation of the Mandelbrot program
from the Programming Rosetta Stone, see
Compile the program with:
gcc -o mandelbrot -O4 mandelbrot.c
andrejbauer / algebra.v
Last active Aug 10, 2020
Uinversal algebra in Coq
View algebra.v
(* An initial attempt at universal algebra in Coq.
Author: Andrej Bauer <>
If someone knows of a less painful way of doing this, please let me know.
We would like to define the notion of an algebra with given operations satisfying given
equations. For example, a group has of three operations (unit, multiplication, inverse)
and five equations (associativity, unit left, unit right, inverse left, inverse right).
andrejbauer /
Last active Jan 20, 2020
How to formulate and prove the statement "all functions are continuous" in an effectful functional language?

Are all functions continuous?

Mathematical background

Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.

Definition: A functional f : (N → N) → N is continuous at a : N → N when there exists m : N such that, for all b : N → N, if ∀ k < m, a k = b k then f a = f b.

andrejbauer / algebraic.v
Last active Jan 15, 2020
Unions of algebraic sets are algebraic
View algebraic.v
(* A Coq formalization of the theorem that the the union of algebraic sets are algebraic.
The file is self-contained, so we start with some general definitions
and facts from logic and sets, and basic algebraic definitions.
It should be straight-forward to translate it to any setting that has
a decent library of basic facts of logic, set theory and algebra.
(* We formalize the following "paper" proof.
andrejbauer /
Last active Jan 15, 2020
A bijection between numbers and pairs of numbers.

A bijection between numbers and pairs of numbers

Every once in a while I am faced with someone who denies that the rational numbers (or fractions, or pairs of integers) can be put into a bijective correspondence with natural numbers. To deal with the situation, I coded up the bijection. So now I can just say: "Really? Interesting. Please provide a pair of numbers (i,j) which is not enumerated by f, as defined in my gist." I am still waiting for a valid counter-example.

Anyhow, here is a demo of f and g at work. I am using the Python version, but a Haskell variant is included as well.

The 100-th pair is:

>>> f(100)
(10, 4)
andrejbauer / topology.v
Last active Oct 22, 2019
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
View topology.v
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
Definition P (A : Type) := A -> Prop.
andrejbauer /
Created Aug 14, 2019
Pictures of algebraic numbers
# Compute algebraic numbers in the complex plane and draw a nice picture
import numpy
import sys
import argparse
import math
import cairo
import pickle
You can’t perform that action at this time.