Metadata-Version: 2.1
Name: proofs
Version: 0.0.3
Summary: Mathematical proof assistant for students and amateurs.
Home-page: https://github.com/maxtheman/proofs
Author: maxtheman
Author-email: proofs@growth.wtf
License: Apache Software License 2.0
Keywords: nbdev jupyter notebook python
Platform: UNKNOWN
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Natural Language :: English
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: License :: OSI Approved :: Apache Software License
Requires-Python: >=3.7
Description-Content-Type: text/markdown
Requires-Dist: anyio (==3.7.0)
Requires-Dist: appnope (==0.1.3)
Requires-Dist: argon2-cffi (==21.3.0)
Requires-Dist: argon2-cffi-bindings (==21.2.0)
Requires-Dist: arrow (==1.2.3)
Requires-Dist: asttokens (==2.2.1)
Requires-Dist: astunparse (==1.6.3)
Requires-Dist: async-lru (==2.0.2)
Requires-Dist: attrs (==23.1.0)
Requires-Dist: Babel (==2.12.1)
Requires-Dist: backcall (==0.2.0)
Requires-Dist: beautifulsoup4 (==4.12.2)
Requires-Dist: bleach (==6.0.0)
Requires-Dist: certifi (==2023.5.7)
Requires-Dist: cffi (==1.15.1)
Requires-Dist: charset-normalizer (==3.1.0)
Requires-Dist: comm (==0.1.3)
Requires-Dist: debugpy (==1.6.7)
Requires-Dist: decorator (==5.1.1)
Requires-Dist: defusedxml (==0.7.1)
Requires-Dist: exceptiongroup (==1.1.1)
Requires-Dist: execnb (==0.1.5)
Requires-Dist: executing (==1.2.0)
Requires-Dist: fastcore (==1.5.29)
Requires-Dist: fastjsonschema (==2.17.1)
Requires-Dist: fqdn (==1.5.1)
Requires-Dist: ghapi (==1.0.3)
Requires-Dist: idna (==3.4)
Requires-Dist: importlib-metadata (==6.6.0)
Requires-Dist: importlib-resources (==5.12.0)
Requires-Dist: ipykernel (==6.23.1)
Requires-Dist: ipython (==8.12.2)
Requires-Dist: isoduration (==20.11.0)
Requires-Dist: jedi (==0.18.2)
Requires-Dist: Jinja2 (==3.1.2)
Requires-Dist: json5 (==0.9.14)
Requires-Dist: jsonpointer (==2.3)
Requires-Dist: jsonschema (==4.17.3)
Requires-Dist: jupyter-events (==0.6.3)
Requires-Dist: jupyter-lsp (==2.2.0)
Requires-Dist: jupyter-client (==8.2.0)
Requires-Dist: jupyter-core (==5.3.0)
Requires-Dist: jupyter-server (==2.6.0)
Requires-Dist: jupyter-server-terminals (==0.4.4)
Requires-Dist: jupyterlab (==4.0.1)
Requires-Dist: jupyterlab-pygments (==0.2.2)
Requires-Dist: jupyterlab-quarto (==0.1.45)
Requires-Dist: jupyterlab-server (==2.22.1)
Requires-Dist: MarkupSafe (==2.1.2)
Requires-Dist: matplotlib-inline (==0.1.6)
Requires-Dist: mistune (==2.0.5)
Requires-Dist: mpmath (==1.3.0)
Requires-Dist: nbclient (==0.8.0)
Requires-Dist: nbconvert (==7.4.0)
Requires-Dist: nbdev (==2.3.12)
Requires-Dist: nbformat (==5.9.0)
Requires-Dist: nest-asyncio (==1.5.6)
Requires-Dist: notebook-shim (==0.2.3)
Requires-Dist: overrides (==7.3.1)
Requires-Dist: packaging (==23.1)
Requires-Dist: pandocfilters (==1.5.0)
Requires-Dist: parso (==0.8.3)
Requires-Dist: pexpect (==4.8.0)
Requires-Dist: pickleshare (==0.7.5)
Requires-Dist: pkgutil-resolve-name (==1.3.10)
Requires-Dist: platformdirs (==3.5.1)
Requires-Dist: prometheus-client (==0.17.0)
Requires-Dist: prompt-toolkit (==3.0.38)
Requires-Dist: psutil (==5.9.5)
Requires-Dist: ptyprocess (==0.7.0)
Requires-Dist: pure-eval (==0.2.2)
Requires-Dist: pycparser (==2.21)
Requires-Dist: Pygments (==2.15.1)
Requires-Dist: pyrsistent (==0.19.3)
Requires-Dist: python-dateutil (==2.8.2)
Requires-Dist: python-json-logger (==2.0.7)
Requires-Dist: pytz (==2023.3)
Requires-Dist: PyYAML (==6.0)
Requires-Dist: pyzmq (==25.1.0)
Requires-Dist: requests (==2.31.0)
Requires-Dist: rfc3339-validator (==0.1.4)
Requires-Dist: rfc3986-validator (==0.1.1)
Requires-Dist: Send2Trash (==1.8.2)
Requires-Dist: six (==1.16.0)
Requires-Dist: sniffio (==1.3.0)
Requires-Dist: soupsieve (==2.4.1)
Requires-Dist: stack-data (==0.6.2)
Requires-Dist: sympy (==1.12)
Requires-Dist: terminado (==0.17.1)
Requires-Dist: tinycss2 (==1.2.1)
Requires-Dist: tomli (==2.0.1)
Requires-Dist: tornado (==6.3.2)
Requires-Dist: traitlets (==5.9.0)
Requires-Dist: typing-extensions (==4.6.2)
Requires-Dist: uri-template (==1.2.0)
Requires-Dist: urllib3 (==2.0.2)
Requires-Dist: watchdog (==3.0.0)
Requires-Dist: wcwidth (==0.2.6)
Requires-Dist: webcolors (==1.13)
Requires-Dist: webencodings (==0.5.1)
Requires-Dist: websocket-client (==1.5.2)
Requires-Dist: zipp (==3.15.0)
Provides-Extra: dev

# proofs

<!-- WARNING: THIS FILE WAS AUTOGENERATED! DO NOT EDIT! -->

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

``` sh
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

``` python
# Start by defining your domain
arbitrary_x = variable("x")
expression = arbitrary_x + 2
```

``` python
print(expression)
```

    x + 2

``` python
# 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.

``` python
# Then define your goal
contradiction_goal = not_equals(expression, arbitrary_x)
```

``` python
@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)


