Alpha Geometry: A wow paper from Nature

34 views
Skip to first unread message

Edward K. Ream

unread,
Jan 20, 2024, 3:01:32 PMJan 20
to leo-editor
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

unread,
Jan 20, 2024, 3:14:05 PMJan 20
to leo-editor


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

unread,
Jan 20, 2024, 3:21:23 PMJan 20
to leo-editor
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
Reply all
Reply to author
Forward
0 new messages