[FOM] Talk on Formal Verification

[Isaac Malitz]

Generalizing on this thread, I would describe much of the 
discussion as being about the following topic "What is the status 
and future of AI in Mathematical Research" (I'll call the topic 
"AI+MathResearch" for short).

I have significant background in AI, but am not a specialist in 
this particular topic. If I were to specialize in this topic, here 
are some top-level questions that would be on my mind:

[a] What are the sub-disciplines of AI that seem most pertinent to 
this topic. (Consider: Common-sense/Extended-Common-sense 
databases, subject-matter-specific
  databases, deep neural networks, ...]

[b] To apply AI to mathematical-research (or any discipline), an 
assessment is needed of that discipline. So for instance, to what 
degree is mathematical research characterized by "gradual 
accumulation and integration of knowledge" rather than 
"breakthrough-insights"? What is the role of heuristics and 
intuition, and how will AI relate to this? The assessments may 
vary for different mathematics sub-disciplines.

[c] Projections about what kinds of progress we will see with 
AI+MathResearch and when. (My professional/technical opinion is 
that some kinds of projections are possible)

[d] From a technical point-of-view, what are the most important 
open problems (or open issues), and what is the current assessment 
of them?

To do a good job with AI+MathResearch, one would have to be expert 
in (some parts of) AI, and also a capable mathematician.
AI+MathResearch is clearly an emerging discipline, extremely 
challenging and interesting, with massive long-term prospects.

Of course there is already activity in this AI+MathResearch.
But does anyone know: What is the status of AI+MathResearch 
overall?
Are there now specialists, teams of specialists, conferences that 
attempt to address [a],[b],[c],[d](and related) in a 
comprehensive, systematic manner?

Of course many FOM'rs (including myself) have opinions about 
various matters; but I am wondering to what degree there is now a 
*discipline* (call it AI+MathResearch or something else) which is 
addressing issues in a comprehensive, systematic manner.

Isaac Malitz
818-231-3965