Alpha Geometry: A wow paper from Nature

[Edward K. Ream]

Here is the link.

I was able to access the paper without a subscription. The solution is left as an exercise for the reader.

We haven't seen anything yet :-)

Edward

[Edward K. Ream]

On Saturday, January 20, 2024 at 2:01:32 PM UTC-6 Edward K. Ream wrote:

Here is the link.

From Figure 3:

a, We first sample a large set of random theorem premises.

b, We use the symbolic deduction engine to obtain a deduction closure.

This returns a directed acyclic graph of statements.

For each node in the graph, we perform traceback to find its minimal set of necessary premise and dependency deductions.

Edward

[Edward K. Ream]

On Saturday, January 20, 2024 at 2:14:05 PM UTC-6 Edward K. Ream wrote:

From Figure 3:

a, We first sample a large set of random theorem premises.

b, We use the symbolic deduction engine to obtain a deduction closure.

This returns a directed acyclic graph of statements.

I read the caption before the introduction, which provides better context:

QQQ

Next we use a symbolic deduction engine on the sampled premises.

The engine quickly deduces new true statements by following forward inference rules as shown in Fig. 3b. This returns a directed acyclic graph of all reachable conclusions.

Each node in the directed acyclic graph is a reachable conclusion, with edges connecting to its
parent nodes thanks to the traceback algorithm described in Methods. This allows a traceback process to run recursively starting from any node N, at the end returning its dependency subgraph G(N), with its
root being N and its leaves being a subset of the sampled premises.

Denoting this subset as P, we obtained a synthetic training example

(premises, conclusion, proof) = (P, N, G(N)).

QQQ

Edward