Email Gateway (Jul 08 2025 at 09:55): Email Gateway (Jul 08 2025 at 09:55):From: Harry Butterworth <heb1001@gmail.com>
Google have set this up now:
Activity · google-deepmind/formal-conjectures · GitHub
https://github.com/google-deepmind/formal-conjectures/activity
On Fri, 23 Aug 2024 at 09:12, Alex Shkotin <alex.shkotin@gmail.com> wrote:
Harry,
Let me add that IMHO the structure of theory storage should be changed to
more granulated than file.Please have a look at some initial proposals [1] where undirected graph
theory was taken as an example to formalize using knowledge unit ideas: the
theory (including proofs), the structure (ugraph), the task and task's
solution.To say it simply it should be DB or KB to keep theory, structures (for
theory is about), and tasks (problems) properly for world wide access.Alex
[1]
https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1чт, 22 авг. 2024 г. в 15:13, Harry Butterworth <heb1001@gmail.com>:
I expect this has been obvious to many of you for some time but it
occurred to me today when thinking about systems like AlphaProof [1] that,
with advances in AI, it might soon become the case that the limiting factor
in solving new mathematical problems could be the availability of unsolved
but peer-reviewed and generally accepted formal problem statements.I thought it might be worth pointing out that a collection of such
statements would be a valuable thing and each one might eventually
constitute the major part of the human effort of actually solving the
problem so ought to earn some recognition in the event it is successfully
completed.An advantage of having a whole collection of problems is that it’s
unlikely to be obvious which problems a new AI is going to be able to
solve, so a larger set would increase the chance of getting lucky with a
mathematical breakthrough.Is there an existing archive of formally specified unsolved
problems? If not, perhaps it would be worth setting one up or maybe adding
an unsolved section to the AFP.This side of things is relatively challenging for AI developers
without the domain specific mathematics knowledge but, presumably,
relatively easy for mathematicians.[1]
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Email Gateway (Jul 08 2025 at 11:21):From: Alex Shkotin <alex.shkotin@gmail.com>
This is interesting. The idea seems to be enjoying success, although it is
rather strange. Since a hypothesis is a unit of knowledge of a developing
theory. Each of the hypotheses placed in this repo will be duplicated by
those who build the theory itself. And the simplest crawler could collect
unproven theorems from all theories.
Thanks for the link.
вт, 8 июл. 2025 г. в 12:54, Harry Butterworth <heb1001@gmail.com>:
Google have set this up now:
Activity · google-deepmind/formal-conjectures · GitHub
https://github.com/google-deepmind/formal-conjectures/activityOn Fri, 23 Aug 2024 at 09:12, Alex Shkotin <alex.shkotin@gmail.com> wrote:
Harry,
Let me add that IMHO the structure of theory storage should be changed to
more granulated than file.Please have a look at some initial proposals [1] where undirected graph
theory was taken as an example to formalize using knowledge unit ideas: the
theory (including proofs), the structure (ugraph), the task and task's
solution.To say it simply it should be DB or KB to keep theory, structures (for
theory is about), and tasks (problems) properly for world wide access.Alex
[1]
https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1чт, 22 авг. 2024 г. в 15:13, Harry Butterworth <heb1001@gmail.com>:
I expect this has been obvious to many of you for some time but it
occurred to me today when thinking about systems like AlphaProof [1] that,
with advances in AI, it might soon become the case that the limiting factor
in solving new mathematical problems could be the availability of unsolved
but peer-reviewed and generally accepted formal problem statements.I thought it might be worth pointing out that a collection of such
statements would be a valuable thing and each one might eventually
constitute the major part of the human effort of actually solving the
problem so ought to earn some recognition in the event it is successfully
completed.An advantage of having a whole collection of problems is that it’s
unlikely to be obvious which problems a new AI is going to be able to
solve, so a larger set would increase the chance of getting lucky with a
mathematical breakthrough.Is there an existing archive of formally specified unsolved
problems? If not, perhaps it would be worth setting one up or maybe adding
an unsolved section to the AFP.This side of things is relatively challenging for AI developers
without the domain specific mathematics knowledge but, presumably,
relatively easy for mathematicians.[1]
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Last updated: Jul 26 2025 at 12:43 UTC