# 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)
Raw data
{
"_id": null,
"home_page": "https://github.com/maxtheman/proofs",
"name": "proofs",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.7",
"maintainer_email": "",
"keywords": "nbdev jupyter notebook python",
"author": "maxtheman",
"author_email": "proofs@growth.wtf",
"download_url": "https://files.pythonhosted.org/packages/0a/c8/7a5625546f1c3c23b12ea39fd57b9ecc231509a4f53c8737b2e16dc129da/proofs-0.0.3.tar.gz",
"platform": null,
"description": "# proofs\n\n<!-- WARNING: THIS FILE WAS AUTOGENERATED! DO NOT EDIT! -->\n\nThis is a proofs validator to help students and hobbyists do\nmathematical thinking and problem solving.\n\nIt\u2019s for when you buy a math book from the local used book store, so you\nhave a piece of software to use to explore the mathematical concepts\nalongside you that\u2019s fun and easy to use for anybody with a programming\nbackground.\n\nIt\u2019s supposed to validate what you\u2019re doing in a \u201cblack box\u201d kind of\nmanner, and try to offer you guardrails enough that you can spot your\nmistakes and feel *reasonably* more confident you know what you\u2019re\ndoing.\n\nNot perfectly confident, reasonably.\n\n#### Features:\n\n- human-readable proofs that run in code. Clear from each line what is\n being achieved mathematically.\n- Pure python. Duck typing and abstracts allow for quick end-to-end\n proof designs, only implementing what you need.\n- Relies on python abstractions you know, like the type system for\n defining input and output types\n- Great, human readable errors so it\u2019s clear where your logic is\n breaking down, why, how you might fix it.\n\n#### Principles\n\n- Minimal abstractions, small API\n- minimal dependencies (just sympy right now)\n- declarative, functional api\n- simple to use\n- batteries included\n\n## Install\n\n``` sh\npip install proofs\n```\n\n## How to use\n\nLet\u2019s start with something simple, first, let\u2019s prove that \u201cGiven x,\nAssume x + 1 = x is false for all x\u201d\n\nThis should be obvious, which makes is great to show how to approach a\nproof.\n\n1. Define the problem\n2. Look at examples\n3. Decide on a proof strategy\n4. Write the proof\n\n``` python\n# Start by defining your domain\narbitrary_x = variable(\"x\")\nexpression = arbitrary_x + 2\n```\n\n``` python\nprint(expression)\n```\n\n x + 2\n\n``` python\n# select a few examples from the reals\nmake_examples('real', 3, expression)\n```\n\n [(-39, -37), (-13, -11), (7, 9)]\n\nHopefully these examples convice us that the statement is false. This\nsuggests that we can prove it by contradiction.\n\n``` python\n# Then define your goal\ncontradiction_goal = not_equals(expression, arbitrary_x)\n```\n\n``` python\n@contradiction_proof\ndef proof_of_x_plus_one(x):\n # Given x, Assume x + 1 = x is true for arbitrary x\n assumed_eq = equals(x + 1, x)\n\n # Calculate x + 1\n next = x + 1\n\n # Observing x + 1 != x, we have reached a contradiction\n return not_equals(next, assumed_eq.rhs)\n\n#Select an arbitrary x from the domain\nprove(contradiction_goal, proof_of_x_plus_one, arbitrary_x)\n```\n\n$$\\mathtt{\\text{Given x, Assume x + 1 = x is true for arbitrary x}}$$\n\n$$x + 1 = x$$\n\n$$\\mathtt{\\text{Calculate x + 1}}$$\n\n$$x + 1$$\n\n$$\\mathtt{\\text{Observing x + 1 != x, we have reached a contradiction}}$$\n\n Proof failed: Derived result Ne(x + 1, x) does not match goal Ne(x + 2, x)\n Check your assumptions and proof function for errors.\n\n False\n\nWith this, we get:\n\n1. Complete latex rendering of the math we are doing in python and our\n logic\n2. validation that what we are returning from the proof matches the\n expected goal\n3. some additional helpful errors\n\n# Next steps\n\nLikes:\n\n- simple API\n\n- structure is about proving things now\n\n- Like that the goal is to create a prove function that matches the goal\n given the input you have. I think that\u2019s very straightforward.\n\nDislikes\n\n- type system not doing anything. Can we use mypy or isinstance to\n actually check that the correct type is being returned?\n\n- no error handling to help detect where the proof is going wrong.\n should provide better error messages than just\n `AttributeError: 'BooleanFalse' object has no attribute 'lhs'` \u2014 why\n is that a booleanFalse object? what else might I want to try? Also\n needs to be build into library, not user defined all the time\n\nMust haves:\n\n- Needs to be clearer that the flow is to generate a proof spec, decide\n on an input, and then generate a proof function to do this. Solve this\n by providing a function that helps do common problem setups, and\n prints them as Latex, then outputs something that can be used in the\n \\_proof strategy decorators.\n\nFeature requests:\n\n- I really want simple, composable visualization features. It will be\n really much more interesting if we can see visually what is happening\n \u2013 see start below\n https://docs.manim.community/en/stable/examples.html#animations\n\n- build in a simple type unification feature. see research on\n \\[\\[proofs - inductive types and unification\\]\\]\n\n- better latex printing\n\nnice to haves\n\n- some common \u2018tactics\u2019 mirroring lean; rewrite, reflexivity, etc. Pull\n from sympy as well\n- integrate hypothesis to show that the\n\nContent:\n\n- clone the natural numbers game\n https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=1\n (good start)\n- companion guide to https://www.people.vcu.edu/~rhammack/BookOfProof/\n- Some hilltop problems\n - https://www.youtube.com/watch?v=IUTGFQpKaPU - ask bard for a proof.\n- other books to read through\n - https://infinitedescent.xyz/about/\n - https://www.math.cmu.edu/~jmackey/151_128/bws_book.pdf\n - https://abstractmath.org/CTCS/CTCS.pdf\n- Another proof project, this one more in line with the philosophy of\n what I\u2019m doing:\n - https://us.metamath.org/mpeuni/mmset.html (very good resource for\n the level of rigor and basicness that I\u2019m looking for)\n\n\n",
"bugtrack_url": null,
"license": "Apache Software License 2.0",
"summary": "Mathematical proof assistant for students and amateurs.",
"version": "0.0.3",
"project_urls": {
"Homepage": "https://github.com/maxtheman/proofs"
},
"split_keywords": [
"nbdev",
"jupyter",
"notebook",
"python"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "e2b696299ae0c1c49e01ee5c6fedeb6662bbbd58bc162cb59be8e5c3ab12fc60",
"md5": "672f01091848c861512901c7e7a114c9",
"sha256": "688f3d6e43fc8aed1f4737afc7b6b4aa95f11f12c65b480a690432ae3fb922f4"
},
"downloads": -1,
"filename": "proofs-0.0.3-py3-none-any.whl",
"has_sig": false,
"md5_digest": "672f01091848c861512901c7e7a114c9",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.7",
"size": 14150,
"upload_time": "2023-06-10T21:09:47",
"upload_time_iso_8601": "2023-06-10T21:09:47.751959Z",
"url": "https://files.pythonhosted.org/packages/e2/b6/96299ae0c1c49e01ee5c6fedeb6662bbbd58bc162cb59be8e5c3ab12fc60/proofs-0.0.3-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "0ac87a5625546f1c3c23b12ea39fd57b9ecc231509a4f53c8737b2e16dc129da",
"md5": "20d99cb15f6ca6d50b2b0324018feb12",
"sha256": "c03a016756df7643d7a66634fae5531cfa9a57d21deb36d0f2cc53f97e43561b"
},
"downloads": -1,
"filename": "proofs-0.0.3.tar.gz",
"has_sig": false,
"md5_digest": "20d99cb15f6ca6d50b2b0324018feb12",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.7",
"size": 17730,
"upload_time": "2023-06-10T21:09:49",
"upload_time_iso_8601": "2023-06-10T21:09:49.660076Z",
"url": "https://files.pythonhosted.org/packages/0a/c8/7a5625546f1c3c23b12ea39fd57b9ecc231509a4f53c8737b2e16dc129da/proofs-0.0.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-06-10 21:09:49",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "maxtheman",
"github_project": "proofs",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"requirements": [
{
"name": "anyio",
"specs": [
[
"==",
"3.6.2"
]
]
},
{
"name": "appnope",
"specs": [
[
"==",
"0.1.3"
]
]
},
{
"name": "argon2-cffi",
"specs": [
[
"==",
"21.3.0"
]
]
},
{
"name": "argon2-cffi-bindings",
"specs": [
[
"==",
"21.2.0"
]
]
},
{
"name": "arrow",
"specs": [
[
"==",
"1.2.3"
]
]
},
{
"name": "asttokens",
"specs": [
[
"==",
"2.2.1"
]
]
},
{
"name": "astunparse",
"specs": [
[
"==",
"1.6.3"
]
]
},
{
"name": "async-lru",
"specs": [
[
"==",
"2.0.2"
]
]
},
{
"name": "attrs",
"specs": [
[
"==",
"23.1.0"
]
]
},
{
"name": "Babel",
"specs": [
[
"==",
"2.12.1"
]
]
},
{
"name": "backcall",
"specs": [
[
"==",
"0.2.0"
]
]
},
{
"name": "beautifulsoup4",
"specs": [
[
"==",
"4.12.2"
]
]
},
{
"name": "bleach",
"specs": [
[
"==",
"6.0.0"
]
]
},
{
"name": "certifi",
"specs": [
[
"==",
"2023.5.7"
]
]
},
{
"name": "cffi",
"specs": [
[
"==",
"1.15.1"
]
]
},
{
"name": "charset-normalizer",
"specs": [
[
"==",
"3.1.0"
]
]
},
{
"name": "click",
"specs": [
[
"==",
"8.1.3"
]
]
},
{
"name": "comm",
"specs": [
[
"==",
"0.1.3"
]
]
},
{
"name": "debugpy",
"specs": [
[
"==",
"1.6.7"
]
]
},
{
"name": "decorator",
"specs": [
[
"==",
"5.1.1"
]
]
},
{
"name": "defusedxml",
"specs": [
[
"==",
"0.7.1"
]
]
},
{
"name": "docutils",
"specs": [
[
"==",
"0.20.1"
]
]
},
{
"name": "execnb",
"specs": [
[
"==",
"0.1.5"
]
]
},
{
"name": "executing",
"specs": [
[
"==",
"1.2.0"
]
]
},
{
"name": "fastcore",
"specs": [
[
"==",
"1.5.29"
]
]
},
{
"name": "fastjsonschema",
"specs": [
[
"==",
"2.17.1"
]
]
},
{
"name": "Flask",
"specs": [
[
"==",
"2.2.2"
]
]
},
{
"name": "fqdn",
"specs": [
[
"==",
"1.5.1"
]
]
},
{
"name": "ghapi",
"specs": [
[
"==",
"1.0.3"
]
]
},
{
"name": "idna",
"specs": [
[
"==",
"3.4"
]
]
},
{
"name": "importlib-metadata",
"specs": [
[
"==",
"5.0.0"
]
]
},
{
"name": "importlib-resources",
"specs": [
[
"==",
"5.12.0"
]
]
},
{
"name": "install",
"specs": [
[
"==",
"1.3.5"
]
]
},
{
"name": "ipykernel",
"specs": [
[
"==",
"6.23.1"
]
]
},
{
"name": "ipython",
"specs": [
[
"==",
"8.12.2"
]
]
},
{
"name": "isoduration",
"specs": [
[
"==",
"20.11.0"
]
]
},
{
"name": "itsdangerous",
"specs": [
[
"==",
"2.1.2"
]
]
},
{
"name": "jaraco.classes",
"specs": [
[
"==",
"3.2.3"
]
]
},
{
"name": "jedi",
"specs": [
[
"==",
"0.18.2"
]
]
},
{
"name": "Jinja2",
"specs": [
[
"==",
"3.1.2"
]
]
},
{
"name": "json5",
"specs": [
[
"==",
"0.9.14"
]
]
},
{
"name": "jsonpointer",
"specs": [
[
"==",
"2.3"
]
]
},
{
"name": "jsonschema",
"specs": [
[
"==",
"4.17.3"
]
]
},
{
"name": "jupyter-events",
"specs": [
[
"==",
"0.6.3"
]
]
},
{
"name": "jupyter-lsp",
"specs": [
[
"==",
"2.1.0"
]
]
},
{
"name": "jupyter_client",
"specs": [
[
"==",
"8.2.0"
]
]
},
{
"name": "jupyter_core",
"specs": [
[
"==",
"5.3.0"
]
]
},
{
"name": "jupyter_server",
"specs": [
[
"==",
"2.5.0"
]
]
},
{
"name": "jupyter_server_terminals",
"specs": [
[
"==",
"0.4.4"
]
]
},
{
"name": "jupyterlab",
"specs": [
[
"==",
"4.0.0"
]
]
},
{
"name": "jupyterlab-pygments",
"specs": [
[
"==",
"0.2.2"
]
]
},
{
"name": "jupyterlab_server",
"specs": [
[
"==",
"2.22.1"
]
]
},
{
"name": "keyring",
"specs": [
[
"==",
"23.13.1"
]
]
},
{
"name": "llama-cpp-python",
"specs": [
[
"==",
"0.1.54"
]
]
},
{
"name": "markdown-it-py",
"specs": [
[
"==",
"2.2.0"
]
]
},
{
"name": "MarkupSafe",
"specs": [
[
"==",
"2.1.1"
]
]
},
{
"name": "matplotlib-inline",
"specs": [
[
"==",
"0.1.6"
]
]
},
{
"name": "mdurl",
"specs": [
[
"==",
"0.1.2"
]
]
},
{
"name": "mistune",
"specs": [
[
"==",
"2.0.5"
]
]
},
{
"name": "more-itertools",
"specs": [
[
"==",
"9.1.0"
]
]
},
{
"name": "mpmath",
"specs": [
[
"==",
"1.3.0"
]
]
},
{
"name": "nbclient",
"specs": [
[
"==",
"0.8.0"
]
]
},
{
"name": "nbconvert",
"specs": [
[
"==",
"7.4.0"
]
]
},
{
"name": "nbdev",
"specs": [
[
"==",
"2.3.12"
]
]
},
{
"name": "nbformat",
"specs": [
[
"==",
"5.8.0"
]
]
},
{
"name": "nest-asyncio",
"specs": [
[
"==",
"1.5.6"
]
]
},
{
"name": "notebook_shim",
"specs": [
[
"==",
"0.2.3"
]
]
},
{
"name": "packaging",
"specs": [
[
"==",
"23.1"
]
]
},
{
"name": "pandocfilters",
"specs": [
[
"==",
"1.5.0"
]
]
},
{
"name": "parso",
"specs": [
[
"==",
"0.8.3"
]
]
},
{
"name": "pexpect",
"specs": [
[
"==",
"4.8.0"
]
]
},
{
"name": "pickleshare",
"specs": [
[
"==",
"0.7.5"
]
]
},
{
"name": "pkginfo",
"specs": [
[
"==",
"1.9.6"
]
]
},
{
"name": "pkgutil_resolve_name",
"specs": [
[
"==",
"1.3.10"
]
]
},
{
"name": "platformdirs",
"specs": [
[
"==",
"3.5.1"
]
]
},
{
"name": "prometheus-client",
"specs": [
[
"==",
"0.16.0"
]
]
},
{
"name": "prompt-toolkit",
"specs": [
[
"==",
"3.0.38"
]
]
},
{
"name": "psutil",
"specs": [
[
"==",
"5.9.5"
]
]
},
{
"name": "ptyprocess",
"specs": [
[
"==",
"0.7.0"
]
]
},
{
"name": "pure-eval",
"specs": [
[
"==",
"0.2.2"
]
]
},
{
"name": "pycparser",
"specs": [
[
"==",
"2.21"
]
]
},
{
"name": "Pygments",
"specs": [
[
"==",
"2.15.1"
]
]
},
{
"name": "pyrsistent",
"specs": [
[
"==",
"0.19.3"
]
]
},
{
"name": "python-dateutil",
"specs": [
[
"==",
"2.8.2"
]
]
},
{
"name": "python-json-logger",
"specs": [
[
"==",
"2.0.7"
]
]
},
{
"name": "pytz",
"specs": [
[
"==",
"2023.3"
]
]
},
{
"name": "PyYAML",
"specs": [
[
"==",
"6.0"
]
]
},
{
"name": "pyzmq",
"specs": [
[
"==",
"25.0.2"
]
]
},
{
"name": "readme-renderer",
"specs": [
[
"==",
"37.3"
]
]
},
{
"name": "requests",
"specs": [
[
"==",
"2.31.0"
]
]
},
{
"name": "requests-toolbelt",
"specs": [
[
"==",
"1.0.0"
]
]
},
{
"name": "rfc3339-validator",
"specs": [
[
"==",
"0.1.4"
]
]
},
{
"name": "rfc3986",
"specs": [
[
"==",
"2.0.0"
]
]
},
{
"name": "rfc3986-validator",
"specs": [
[
"==",
"0.1.1"
]
]
},
{
"name": "rich",
"specs": [
[
"==",
"13.4.1"
]
]
},
{
"name": "Send2Trash",
"specs": [
[
"==",
"1.8.2"
]
]
},
{
"name": "six",
"specs": [
[
"==",
"1.16.0"
]
]
},
{
"name": "sniffio",
"specs": [
[
"==",
"1.3.0"
]
]
},
{
"name": "soupsieve",
"specs": [
[
"==",
"2.4.1"
]
]
},
{
"name": "stack-data",
"specs": [
[
"==",
"0.6.2"
]
]
},
{
"name": "sympy",
"specs": [
[
"==",
"1.12"
]
]
},
{
"name": "terminado",
"specs": [
[
"==",
"0.17.1"
]
]
},
{
"name": "tinycss2",
"specs": [
[
"==",
"1.2.1"
]
]
},
{
"name": "tomli",
"specs": [
[
"==",
"2.0.1"
]
]
},
{
"name": "tornado",
"specs": [
[
"==",
"6.3.2"
]
]
},
{
"name": "traitlets",
"specs": [
[
"==",
"5.9.0"
]
]
},
{
"name": "twine",
"specs": [
[
"==",
"4.0.2"
]
]
},
{
"name": "typing_extensions",
"specs": [
[
"==",
"4.6.0"
]
]
},
{
"name": "uri-template",
"specs": [
[
"==",
"1.2.0"
]
]
},
{
"name": "urllib3",
"specs": [
[
"==",
"2.0.2"
]
]
},
{
"name": "watchdog",
"specs": [
[
"==",
"3.0.0"
]
]
},
{
"name": "wcwidth",
"specs": [
[
"==",
"0.2.6"
]
]
},
{
"name": "webcolors",
"specs": [
[
"==",
"1.13"
]
]
},
{
"name": "webencodings",
"specs": [
[
"==",
"0.5.1"
]
]
},
{
"name": "websocket-client",
"specs": [
[
"==",
"1.5.2"
]
]
},
{
"name": "Werkzeug",
"specs": [
[
"==",
"2.2.2"
]
]
},
{
"name": "zipp",
"specs": [
[
"==",
"3.10.0"
]
]
}
],
"lcname": "proofs"
}
