My name is Carlos E. Freites. I'm Spanish, with a degree in mathematics. If you've made it this far, I'm very happy because it means you value my work. Indeed, I've worked on Mathdialog for over 12 years completely alone. I haven't had any infrastructure to support me, neither in the form of a university, research center, or grant, nor from any foundation or company. However, I have participated in two conferences in the field.
As autonomous and clear as machine-to-human proofs are, they require something pedagogically important: the ability to justify heuristically (not logically) the need to use a logical command at crucial moments in a proof. To achieve this, the option will be given to users of human-to-machine proofs to include such justifications in the form of text or image so that the corresponding machine-to-human proof can use them.
For instance on the proof of INV_GROUP_UNIQUENESS showed in the video, the first step is the use of the GROUP_DIRECT_0 to get
There is one y ∈ G such that e = (y @ x)
The explanation is correct:
Here, we can apply the theorem:
GROUP_DIRECT_0
to get the formula
There is one y ∈ G such that e = (y @ x)
But this doesn't explain why we need this hypothesis. In this case the heuristic would be “The idea is to find a candidate to prove the existential quantifier in the goal.” Of course, the heuristics must be used in really important points in the proof.
As simple as it may seem, this requires a great deal of work, but its usefulness would more than compensate for it.
All these years, I've been funding Mathdialog solely by repairing computers for individuals at their homes. However, mobile phones have largely displaced them, resulting in a now-critical reduction in income for Mathdialog and even for my own livelihood.
That's why I urgently need your support. Do not doubt that I will be infinitely grateful to you.
