What is the general design of these new math solving systems? [D]

Excerpt

From what I've seen online so far, the description of these systems is roughly: They asked the model (often Aster) to generate statements in LEAN and then submit those to a LEAN compiler to be checked. Based on the results of attempting the LEAN compilation, they somehow add those statements as fact. When the full proof in LEAN compiles, the system is finished. I can imagine trying to jam as much of a proof as possible into the context window but some of the papers these systems have produced ar