> ask it to generate Lean 4 proofs based off centimorgans

That's not confidence inspiring. It'll give you proofs I'm sure, but with what assumptions? You need a full blown model for crossover, and even that would hardly help, because you don't know what assumptions went into the segment match. What size segments are filtered out, how many mismatches are ignored, how interpolation is done, how no-calls are treated etc. Let alone the cM value for services which don't give segments! And then there's that the question for instance Bettinger's shared cM project asks (given this relationship, what shared cM level do you expect to see?) is actually very different from the question we most often ask (given this shared cM level, what relationship should I expect?). When you get into the distant cousin range, those questions can be very different indeed. And we're not even getting into endogamy.

They say the first principle is that you must not fool yourself, and you're the easiest person to fool. I'm worried that AI can be really powerful self-fooling tools!!

aha I appreciate the rant, and you obviously know what you are talking about.

I have used the Lean 4 approach and I wasn't proposing it solves the problem, but it has reduced the search space for me in certain circumstances. At best it's a nice way for agents to keep in their context windows potential relations, I made it create enormous amounts of hypothetical nodes and then visualized it so I could talk with my relatives about potential paths.

As a side note, I believe, if we had a better DNA site that had great API access (and exposed genomes), I think agents could probably solve genealogy, even as far as complex endogamics.

(I don't think centimorgans is that useful past 4 generations kind of thing)