Verifiable Reasoning AI for Education – Looking to Connect

General
1

Hi everyone,

I’m building a verifiable reasoning AI system focused on education. The goal is to generate transparent, auditable proof traces that clearly show how a conclusion was reached, plus precise identification of where reasoning fails (especially useful for tutoring flawed or incomplete student thinking).

The core is a deterministic logic engine built in Prolog (using SLD-resolution, unification, and backtracking for natural proof/failure trees). I’m also exploring neuro-symbolic integration and open to modern declarative alternatives (ASP, Datalog, etc.).

I’m currently in the process of making Aliyah and would love to informally connect with people who have experience in:

  • Logic programming / Prolog applications

  • Neuro-symbolic AI

  • Verifiable / explainable reasoning systems

  • Lean or formal methods

Happy to share more details about the architecture privately, exchange ideas, or explore potential collaboration (remote for now, Israel soon).

If this resonates with your interests, feel free to reply or message me.

Thanks!

2

I think there may be some overlap with this project by user @siegfried :

Good luck with your project!

3

Hey @AW9990

This is exactly the kind of thing I’ve been focused on for the last few months. Happy to talk or share ideas. How did you develop this interest?

4

Interesting. I would as well. are you connected with the middle east at all? that is where I am located.

5

Hi,

Teaching might be never the same as before. Especially if you have
to take a calculus course. Terence tao has announced May 31 2025
and now published a Lean formalization of his Analysis I book:

Lean formalization of Analysis I
https://github.com/teorth/analysis

I don’t know how complete it is. Does it have a lot
of proofs by “sorry” ? Before that, amazingly he had
a touch down with E-graphs:

For proving implications, we used another technique called equality
saturation with the lean-egg tactic, to automatically construct proofs.

A similar approach is being pursued in the MagmaEgg tool as well,
which is a standalone program that only supports magma equalities,
while the lean-egg tactic supports any Lean expression.

But I didn’t find a reception of his recent Lean Analysis I work yet.
I only found a background story on Terrence Tao and the
equational theory work he did, after he started using Lean in 2023:

How Terry Tao Became an Evangelist for AI in Math
May 31 2025
https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

Disclaimer: Calling Lean AI might or might not be a stretch.

Bye

6

There’s a group of us that are interested in some of those same topics, Welcome to The Prolog Education Group!