Suppose the goal was to generate code from proofs.
Suppose that certain tactics have "code-like" equivalents.
Can we define such a restricted set of tactics?
This would eliminate Coq's hammer tactic, for example.
The definition of an axiom could include the text for the
equivalent program, making
In general, I'm pretty skeptical of Neural Net generation of math,
but I'm following the literature quite closely.
I recently spent time with an effort that tried to do integration.
It was interesting because they could "round trip" the solution by
differentiating the result. I worked with the
This is an interesting paper (especially given that it
is work under Gilbert Strang):
A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
https://arxiv.org/pdf/2112.15594.pdf
"This work shows that a neural
A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
https://arxiv.org/pdf/2112.15594.pdf
