Metadata-Version: 2.1
Name: proofs
Version: 0.0.1
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
Description: # 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 + 1
        ```
        
        ``` python
        print(expression)
        ```
        
            x + 1
        
        ``` python
        # select a few examples from the reals
        make_examples('real', 3, expression)
        ```
        
            [(-92, -91), (59, 60), (80, 81)]
        
        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 $\neq$ 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)
        ```
        
            <IPython.core.display.Latex object>
        
        $$x + 1 = x$$
        
            <IPython.core.display.Latex object>
        
        $$x + 1$$
        
            <IPython.core.display.Latex object>
        
        $$\text \quad x + 1 \neq x \quad Q.E.D.$$
        
            True
        
        With this, we get: 1. comments converted to latex, along with latex
        rendering of the math we are doing in python 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)
        
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
Provides-Extra: dev
