DeduKt is an open-source mathematical framework, that assists with mathematical work through symbolic computation, interpretive and intelligent proof assitance. The main goals of this project is to design a framework for any kind of mathematical practices, extending it to a point where one would be able to design a new mathematical structure from scratch.
We aim to provide real-time assitance in both proof and symbolic computations using different models and artificial intelligence. Our goal is to design a all-in-one toolkit for mathematical practices in computers, but our initial goal is to develope a symbolic reasoning system for mathematical proof and mathematical computations.
There are many alternatives in this field, namely, Mathematica, MatheSage, Scipy etc for symbolic computation and Coq, Isabelle, Agda, Arenda etc for proof assistance, however these are not in anyway connected to each other for the benefit of both worlds, Mathematica (as a pioneer in symbolic computation) offers no proof assistance during the works in its notebooks, its main focus is to provide functions and simplification methods for current mathematical task. This in my opinion is a downside for mathematica, beside this the age of this system and since it was build in a totally different era might give us an advantage on starting a new one on our own.
Although they are trying to connect this system with Artificial Intelligence, Building such integration for a system that didn't take it into account in the first place might have some troubles. DeduKt on the other hand is being built with Ai in mind which would make it perfect for integrations of such kind.
One of the main aspects of this project is to be able to ground it on collaborative code. Open-source projects are normally backed by a grant or some sort of resource for people to be able to spend time on it. For the starting point for DeduKt, we got no grant, but if the project gets a good reputation in scientific society then we would certainly apply for a grant.
An open source software model supports collaboration on Dedukt from the worldwide mathematical and programming communities. Opening elements of the development process, including source code itself, to review and contribution has numerous benefits. This model fosters innovation by mathematicians and developers as expertise from diverse backgrounds invariably leads to faster progress. Improvements can be contributed by those that specialize in relevant areas, while the community as a whole rapidly surfaces any issues for swift resolution. The freely accessible and adaptable nature of open source code will make Dedukt more flexible and customizable to the evolving needs of mathematical researchers as well. Libraries and knowledge systems often must take on functions unforeseen by original creators. Dedukt's open design and extensible architecture will help avoid obsolescence or limitations imposed by proprietary restrictions.
Lastly, open source provides an avenue to maximize awareness while ensuring this mathematical intelligence system remains freely available for future generations. Visibility of capabilities and code quality for inspection builds trust and interest in the mathematical community critical to Dedukt's success. Licensing it permissively guarantees unfettered ongoing access for mathematicians and developers seeking to utilize leading-edge tools, or push them further via open enhancements.
A community focused on openness and scientific advancement will prove key to rapid advancement and sustained viability moving forward as computational mathematics grows ever more capable and vital for 21st century research breakthroughs. Embracing collaborative open source development principles positions this project to achieve its ambitious goals of crafting the preeminent intelligent software to empower mathematical practitioners.
Proof assistants such as Coq or Isabelle have demonstrated immense value in constructing reliable formal proofs. However, these tools function primarily as verification systems - able to check proofs supplied to them rather than actively participate in proof generation and discovery. The mathematician or programmer must determine relevancy of other proven lemmas and construct an entire skeleton of reasoning before a proof assistant can approve it as logically valid.
Dedukt aims to take computational mathematical collaboration to a new level with built-in intelligence to aid users more extensively throughout the proof development lifecycle. Going beyond passive checking, Dedukt seeks to guide the user interactively. When a proof goal gets troublesome or stalled, Dedukt will suggest relevant lemmas and theorems to consider based on contextual understanding of the target domain.
By actively participating alongside the human to overcome sticking points with automated recommendations, Dedukt can lessen formal proof burdens. The proposed semantic enrichment and inference techniques strive to enable more flexibility for mathematicians while retaining the rigor of computer-verified results - getting them unstuck faster while avoiding logical errors through co-reasoning with this intelligent assistant. This would also come in handy with simplification and symbolic computations, suppose that one writes a formula or an equation which is already known by the system, then based on few hints the system would provide some later steps that the researcher/user would use to get different results.