Lines and Universes
Rethinking how math could be done - through machine-assisted lines and universes. Engineer's perspective.
I will refer to them as 'lines' rather than 'proofs.' Proofs will come later. Think of these lines as checkpoints and initially assign them mundane names (although they can be renamed or labeled - machine-assisted naming could be very effective and standardized).
Lines would be more localized and subject to frequent changes. They would form part of a larger universe. Imagine them as flowers on a vast canvas, representing the universe, or your first open tab.
You would have the ability to view multiple lines simultaneously. They would be interconnected, guiding you through the process. Once the work is completed, everything would turn 'green' (indicating success).
Initially, you would converse with the bot using natural language, Lean syntax, etc., and then receive the first version of the universe, containing all the interconnected lines. Picture this as a Blueprint, but one that's generated by a machine based on your conversation, filled with placeholders (indicated by 'sorry's). If the initial result isn't satisfactory, you could continue the dialogue for improvements.
This would be a highly iterative process. You would address discrepancies between lines based on the bot's ranked recommendations. It would be possible to discard less promising lines while preserving those that are meaningful (and to save your own checkpoints). You could continuously refine all lines and discuss specific lines or groups of lines, as well as the paths – i.e., the faded lines that connect the 'lines' (resembling Lean code).
With each adjustment (modifying a 'sorry') or request made in the chat, the bot would respond by filling in the missing parts to the best of its ability.
You could share your preferred exploration style with the bot (noting that Ramanujan’s style differs from Hardy’s).
Lines would not always be perfectly connected; you'd be creating universes (think visualization of embeddings). The larger the leaps, the more scattered and disconnected the universe would appear. Easing local connectedness requirements would facilitate parallelizing proof (and line) construction.
'Spooky at distance action' would apply — altering a particular checkpoint (of a line) in one place would cause many other lines to change. This effect would need to be color-coded.
Ariadne's thread would also be relevant, providing recommendations for the next step (and subsequent steps) based on the likelihood of impact, given the current state of the universe – that's the path.
Bruteforce (and more intelligent forms of bruteforce) could be useful for quickly “breaking” certain lines.
Imagine a combination of CI/CD, infrastructure as code, an AI bot, Lean, Blueprint with Canva, Git, and Docker (including a Docker registry) applied to mathematics.
Interestingly, proofs would involve not just the final proof structure (without any 'sorry's) but also the related lineage (similar to data lineage in machine learning or a git-tree times tensorboard).
This aspect is crucial. The story becomes part of the final outcome. One could publish just the story and pull from the universe registry to obtain the lineage.
Furthermore, bots could autonomously continue working on the universe.
Let’s examine some line structures (supported by Lean) such as Direct Proof, Proof by Induction, Case Analysis, Proof by Contradiction, and others. Each technique, from tactic-based proofs to automated reasoning tools, will be utilized – think of them as templates. Additionally, one could propose their own templates or structures.
Here’s a short list that can already be done using Lean (I’m still learning Lean, so I might be wrong):
Direct Proof: This technique involves proving a statement by straightforward logical reasoning from axioms or previously proven theorems.
Proof by Induction: This is used to prove statements about natural numbers or other well-founded structures. It involves showing that if a property holds for a base case and assuming it holds for an arbitrary case implies it holds for the next case, then it holds for all cases.
Proof by Cases (Case Analysis): This involves dividing the proof into several cases, often based on the definition of a term or the structure of a mathematical object, and proving the statement separately for each case.
Proof by Contradiction: This technique involves assuming the opposite of what you want to prove, showing that this assumption leads to a contradiction, and thus concluding that the original statement must be true.
Proof by Contraposition: This involves proving an implication by proving its contrapositive.
Constructive Proof (Existence Proof): This provides a constructive method to demonstrate the existence of a mathematical object with a certain property, rather than proving its existence indirectly.
Non-Constructive Proof (Existence Proof without Construct): This proves the existence of an object with certain properties without providing a specific example or method to construct such an object.
Proof by Equivalence: This involves showing that two statements are equivalent, often by proving that each implies the other.
Recursive Definitions and Proofs: This technique defines functions or sets recursively and proves properties about them using induction.
Proof by Unfolding Definitions: This involves proving a statement by expanding it according to the definitions of the terms involved.
Tactic-based Proofs: Lean provides a powerful tactic language for interactive theorem proving, where proofs are constructed step by step using tactics. Each tactic modifies the current proof state towards the goal.
Automated Reasoning Tools: Lean integrates automated reasoning tools and decision procedures that can automatically solve certain types of logical and mathematical problems.
Proof by Simulation and Rewriting: Proving properties by systematically replacing parts of a statement using known equivalences or properties until the statement is reduced to a known truth.
Currently, if one is not engaged with the FLT proof (as it’s not a simple task), attempting to reach a Blueprint with a bot might yield funny results (see my result below).
Although likely incorrect, this represents a valuable starting point.
I hope you enjoyed it!