proofs

Mathematical proof assistant for curious amateurs.

This is a proofs validator to help students and hobbyists do mathematical thinking and problem solving.

It’s for when you buy a math book from the local used book store, so you have a piece of software to use to explore the mathematical concepts alongside you that’s fun and easy to use for anybody with a programming background.

It’s supposed to validate what you’re doing in a “black box” kind of manner, and try to offer you guardrails enough that you can spot your mistakes and feel reasonably more confident you know what you’re doing.

Not perfectly confident, reasonably.

Features:

  • human-readable proofs that run in code. Clear from each line what is being achieved mathematically.
  • Pure python. Duck typing and abstracts allow for quick end-to-end proof designs, only implementing what you need.
  • Relies on python abstractions you know, like the type system for defining input and output types
  • Great, human readable errors so it’s clear where your logic is breaking down, why, how you might fix it.

Principles

  • Minimal abstractions, small API
  • minimal dependencies (just sympy right now)
  • declarative, functional api
  • simple to use
  • batteries included

Install

pip install proofs

How to use

Let’s start with something simple, first, let’s prove that “Given x, Assume x + 1 = x is false for all x”

This should be obvious, which makes is great to show how to approach a proof.

  1. Define the problem
  2. Look at examples
  3. Decide on a proof strategy
  4. Write the proof
# Start by defining your domain
arbitrary_x = variable("x")
expression = arbitrary_x + 2
print(expression)
x + 2
# select a few examples from the reals
make_examples('real', 3, expression)
[(-39, -37), (-13, -11), (7, 9)]

Hopefully these examples convice us that the statement is false. This suggests that we can prove it by contradiction.

# Then define your goal
contradiction_goal = not_equals(expression, arbitrary_x)
@contradiction_proof
def proof_of_x_plus_one(x):
    # Given x, Assume x + 1 = x is true for arbitrary x
    assumed_eq = equals(x + 1, x)

    # Calculate x + 1
    next = x + 1

    # Observing x + 1 != x, we have reached a contradiction
    return not_equals(next, assumed_eq.rhs)

#Select an arbitrary x from the domain
prove(contradiction_goal, proof_of_x_plus_one, arbitrary_x)

\[\mathtt{\text{Given x, Assume x + 1 = x is true for arbitrary x}}\]

\[x + 1 = x\]

\[\mathtt{\text{Calculate x + 1}}\]

\[x + 1\]

\[\mathtt{\text{Observing x + 1 != x, we have reached a contradiction}}\]

Proof failed: Derived result Ne(x + 1, x) does not match goal Ne(x + 2, x)
Check your assumptions and proof function for errors.
False

With this, we get:

  1. Complete latex rendering of the math we are doing in python and our logic
  2. validation that what we are returning from the proof matches the expected goal
  3. some additional helpful errors

Next steps

Likes:

  • simple API

  • structure is about proving things now

  • Like that the goal is to create a prove function that matches the goal given the input you have. I think that’s very straightforward.

Dislikes

  • type system not doing anything. Can we use mypy or isinstance to actually check that the correct type is being returned?

  • no error handling to help detect where the proof is going wrong. should provide better error messages than just AttributeError: 'BooleanFalse' object has no attribute 'lhs' — why is that a booleanFalse object? what else might I want to try? Also needs to be build into library, not user defined all the time

Must haves:

  • Needs to be clearer that the flow is to generate a proof spec, decide on an input, and then generate a proof function to do this. Solve this by providing a function that helps do common problem setups, and prints them as Latex, then outputs something that can be used in the _proof strategy decorators.

Feature requests:

  • I really want simple, composable visualization features. It will be really much more interesting if we can see visually what is happening – see start below https://docs.manim.community/en/stable/examples.html#animations

  • build in a simple type unification feature. see research on [[proofs - inductive types and unification]]

  • better latex printing

nice to haves

  • some common ‘tactics’ mirroring lean; rewrite, reflexivity, etc. Pull from sympy as well
  • integrate hypothesis to show that the

Content:

  • clone the natural numbers game https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=1 (good start)
  • companion guide to https://www.people.vcu.edu/~rhammack/BookOfProof/
  • Some hilltop problems
    • https://www.youtube.com/watch?v=IUTGFQpKaPU - ask bard for a proof.
  • other books to read through
    • https://infinitedescent.xyz/about/
    • https://www.math.cmu.edu/~jmackey/151_128/bws_book.pdf
    • https://abstractmath.org/CTCS/CTCS.pdf
  • Another proof project, this one more in line with the philosophy of what I’m doing:
    • https://us.metamath.org/mpeuni/mmset.html (very good resource for the level of rigor and basicness that I’m looking for)