A pilot project in universal algebra to explore new ways to collaborate
Terence Tao's pilot project in universal algebra aims to enhance collaboration in mathematical research using machine assistance, exploring equational theories for magmas and streamlining the verification process through crowdsourcing.
Read original article
Terence Tao has proposed a pilot project in universal algebra aimed at enhancing collaboration in mathematical research through machine assistance. Traditional mathematical projects typically involve a small group of experts who can verify each other's contributions, making it difficult to scale up projects or include public contributions due to the complexity and potential for errors. The introduction of proof assistant languages like Lean could facilitate larger collaborations by allowing modular contributions from both professional mathematicians and the public, as well as automated tools. Tao suggests that this approach could be applied not only to formalizing existing mathematics but also to exploring new mathematical problems. He specifically proposes investigating equational theories for magmas, which are sets equipped with a binary operation. The project aims to expand the implications and non-implications among various equational axioms, potentially leading to a more extensive understanding of their relationships. By crowdsourcing the exploration of these axioms and utilizing automated tools, the project seeks to streamline the verification process and enhance the scalability of mathematical research.
- Terence Tao proposes a pilot project in universal algebra to enhance collaboration using machine assistance.
- The project aims to explore equational theories for magmas, focusing on the implications among various equational axioms.
- Proof assistant languages like Lean could facilitate contributions from both experts and the public.
- The project seeks to crowdsource the exploration of mathematical problems, potentially leading to new discoveries.
- The initiative aims to streamline the verification process and improve the scalability of mathematical research.
Related
Can the New Mathstral LLM Accurately Compare 9.11 and 9.9?
Mathstral is a new 7B model by Mistral AI for math reasoning, with a 32k context window and Apache 2.0 license. It aims to improve common sense in math problem-solving, deployable locally with LlamaEdge and shareable via GaiaNet for customization and integration.
LeanDojo: Theorem Proving in Lean Using Language Models
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches. It includes benchmarks and enables interactive proof state observation, improving automation and discovering new proofs.
LeanDojo: Theorem Proving in Lean Using LLMs
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches, and includes benchmarks for training machine learning models in theorem proving.
Knuckledragger, a Semi-Automated Python Proof Assistant
The "Knuckledragger" project is a semi-automated Python proof assistant based on Z3, focusing on usability and various mathematical theories, with open-source code and documentation available on GitHub.
Ask HN: Programmers Who Want to Get Better at Math
The Awesome Math creator seeks input from programmers and engineers to improve math skills for machine learning, data science, and graphics programming, focusing on challenges and preferred learning resources.
7 commentsThe project as described in the article is to produce a graph (Poset) where each node is a law (say the commutativity equation for example) and each edge is either a proof of implication or a proof of a non-implication, since this graph is infinite the project limits the laws considered to up to 4 applications of the binary operator.
The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.
The collaborative aspect of the project is to write a proof for each kind of edge (implication and not_implications) between the 4694 considered nodes.
There's also the advantage that a GitHub CI running lean will be setup to automatically check if the pull requests adding theses edges are right or wrong without the need for a human to do the checking of the proofs in their head.
partial visualization of the (WIP) graph: https://github.com/teorth/equational_theories/blob/0e67dad3b...
outline of the project: https://teorth.github.io/equational_theories/blueprint/
github repo: https://github.com/teorth/equational_theories
> So, the situation here is somewhat similar to the Busy Beaver Challenge, in that past a certain point of complexity, we would necessarily encounter unsolvable problems
I must be a platonist to squirm about this. There are no unsolvable problems with undecidability or busy beaver numbers. The only thing is some math questions are actually infinitely many problems disguised as a single problem.
The halting problem etc is the opposite of unsolvable, it’s so solvable humanity can never finish solving it. It’s infinitely solvable.
It’s as if we found a magical soup which has a new taste every day forever, and we call it “untasteable”. It’s not untasteable! It’s the tastiest thing ever!
Perhaps a hopefully-compressible correlation matrix, sorted and collapsed on similarity, with mouseover to get equations?
Related
Can the New Mathstral LLM Accurately Compare 9.11 and 9.9?
Mathstral is a new 7B model by Mistral AI for math reasoning, with a 32k context window and Apache 2.0 license. It aims to improve common sense in math problem-solving, deployable locally with LlamaEdge and shareable via GaiaNet for customization and integration.
LeanDojo: Theorem Proving in Lean Using Language Models
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches. It includes benchmarks and enables interactive proof state observation, improving automation and discovering new proofs.
LeanDojo: Theorem Proving in Lean Using LLMs
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches, and includes benchmarks for training machine learning models in theorem proving.
Knuckledragger, a Semi-Automated Python Proof Assistant
The "Knuckledragger" project is a semi-automated Python proof assistant based on Z3, focusing on usability and various mathematical theories, with open-source code and documentation available on GitHub.
Ask HN: Programmers Who Want to Get Better at Math
The Awesome Math creator seeks input from programmers and engineers to improve math skills for machine learning, data science, and graphics programming, focusing on challenges and preferred learning resources.