Trinity: An Autoformalization System for Verified Superintelligence

[alex.shkotin]

FYI from Anatoly Levenchuk  findings: " Trinity systematically processes entire papers, intelligently corrects its own formalization errors by analyzing failed attempts, and automatically refactors lengthy proofs to extract useful lemmas and abstractions. This results in independently verifiable mathematical knowledge that requires no trust in the AI system itself.  "

https://www.morph.so/blog/trinity

I hope we should wait a little for other kind of sciences and technologies as math is the most ready ;-)

Alex

[Neven Knezevic]

To your point, Alex, formalized proofs generated on the fly have incredible utility in physics, but also in bioinformatics, and in formal verification of code. 

I would like to see a conversational theorem prover that is suitable for verification and exploration. 

It is admirable to see the machine-generated proof from the paper "The abc Conjecture Is True Almost Always", but I feel this is not enough. 

The goal is to see these kinds of proofs generated on the fly, by an LLM, in a conversational setting. 

Formal ontology will get a substantial boost from this, as formally-verified ontologies that are auto-generated will give us all huge gains in utility and accuracy. 

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/5c0f8213-eede-4f5a-bcef-7d75779302f9n%40googlegroups.com.

[John F Sowa]

Neven, Alex, Anatoly,

These systems are very useful and they are getting better.  But they are very, very far from superintelligence.  Unfortunately, they often punish their users with superstupidity.

My colleague Arun Majumdar and I have written and spoken a great deal about these systems, and there is much, much more to say.    For a summary, see my Ontolog Forum talk, which is now on YouTube: "Without  ontologies, LLMs are clueless" from 2024, This got more than 10K downloads.   Just google "John Sowa YouTube" and it's the first hit.

I'm now writing an article that goes into more detail, and I'll send an excerpt next week.

John

 

---

From: "Neven Knezevic" <con...@neven.me>

[Neven Knezevic]

John, 

I do not think we need superintelligence to achieve satisfying results from a conversational theorem prover. 

Will such functionality be needed for proper superintelligence? 

I have no doubts formal verification on the fly is something one should expect from a superintelligence. 

That is, assuming someone can pin down the requirements and not have it be a nebulous hype train. I'd rather we look for the lower hanging fruit first. 

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/cd1e33a53bc94c7a97dfb4cf89d7c48d%40042d8d12b79e4ba29a92ed728b680bf6.

[Alex Shkotin]

Neven,

If you have any links to examples of formalized proofs, not necessarily generated on the fly in physics or bioinformatics, please share with us.

To rephrase JFS, let me say: "Without formal theories, LLMs are clueless."

But IMHO, formalizing theories is a creative endeavor in which AI is only an auxiliary but powerful tool.

Alex

вс, 15 июн. 2025 г. в 00:39, Neven Knezevic <con...@neven.me>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CA%2BNDXXSy4yWA4XsKXm8vR6%3DNPaYJvLeyatSvFo%2BotZB4FAAJ-g%40mail.gmail.com.

[Neven Knezevic]

Alex,

For the referenced paper on the formalized ABC conjecture, see the arXiv link: https://arxiv.org/pdf/2505.13991

For the Lean formalization of said paper, see here: https://github.com/morph-labs/lean-abc-true-almost-always/blob/main/ABCTrueAlmostAlways/ABCTrueAlmostAlways.lean

Aside from the above paper referenced in the Trinity website, here are some more examples:

A Lean copilot: https://github.com/lean-dojo/LeanCopilot

A preprint containing examples of auto-generated proofs: https://arxiv.org/html/2503.04772v1

Lean and formal ontology go well together already as well, so it is not a stretch to imagine we can further specify various data models in Lean. 

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORuy9961Nz8TdAh_Ujn%3DeH%3DDCgSzk5qN%2BXLRjoTUve3%3DA%40mail.gmail.com.

[John F Sowa]

Neven, Alex, List,

I certainly agree with that point:

NK:  I do not think we need superintelligence to achieve satisfying results from a conversational theorem prover. 

Of course not.   Our old VivoMind company achieved that capability over a dozen years ago.  Wolfram's company also achieved related results around that time.  In fact, our VivoMind company got a free copy of Wolfram's software because we had some joint projects.  See https://jfsowa.com/talks/cogmem.pdf . 

Skip to slide 44 for the applications.  For a description of the technology for analyzing languages, start at slide 2.   No system based only on LLMs can do any of those applications.  But our new Permion Inc. company combines the best of that symbolic teechnology with LLMs,

If you want evidence that LLMs, by themselves are stupid, just google "Kenyan workers on chatgpt".   You'll get many hits about how they paid them $2 per hour to detect many variations of porn and other kinds of depravity on WWW sites.  Those workers said that working for days on end reading that horror created nightmares and worse.  

Many of them quit after a few days.  Others continued because they needed the money.   But all that work showed that underpaid Kenyan workers are MORE INTELLIGENT than the latest and greatest developments by ChatGPT. 

There is much more that needs to be said, but don't believe anybody who tells you that superintelligence is just around the corner.

John

PS:  If you want to know why you can't buy a VivoMind or Permion system today, the answer is simple;  It takes a huge amount of work that can be supported by a large gov't agency that has powerful computers to run the stuff.  But designing something that can run in anybody's cell phone takes at least a hundred times more work.  We're working to build such systems, but there is a huge gap between a proof of concept and an application on a cell phone.

[John F Sowa]

Arun sent the following reply.  But since he is not an Ontolog subscriber, I'm forwarding his note.

As you might note from the prices in Arun's link, only companies or gov't agencies with deep pockets can afford the products.  But our ultimate goal is to produce products that ordinary people can buy (or rent) and use.  But it takes a great deal of funding to do the R & D that can produce such products.

John

 

---

From: "Arun Majumdar" <ar...@permion.ai>
Sent: 6/15/25 6:08 PM

Also, we are actually available on the AMAZON (AWS MARKETPLACE) Cloud.

 https://aws.amazon.com/marketplace/search/results?searchTerms=permion

 But good AI is quite expensive as you will notice.

 Cheers!

[Alex Shkotin]

Neven,

My question is about practical formalization results beyond math, where we have hundreds of theories formalized not only on Lean but for example on Isabelle https://www.isa-afp.org/.

So we should ask for different sciences about the achievements of formalization there.

I asked you about physics and bioinformatics because you mentioned these sciences.

As the result for Document engineering let me refer to https://github.com/logicalhacking/Isabelle_DOF

For formal theory of Context-Free Grammars have a look at https://www.isa-afp.org/entries/Context_Free_Grammar.html 

We take theory. We formalize it. 

For the way to keep together different formalizations look here (PDF) Theory framework - knowledge hub message #1.

Sorry, I am not interested in "Generating Millions Of Lean Theorems With Proofs".

I am interested, for example, in formalization of classical Mechanics beginning with Statics. And for formalization of any axiomatic theory of euclidean geometry, for ex. Hilbert's one.

For fun look here https://www.linkedin.com/analytics/post-summary/urn:li:activity:7339547265801355265/

So if you have references on results about formalization of theoretical knowledge in natural sciences, please share.

To get more about physics in Isabelle we can do this https://www.isa-afp.org/search/?s=physics

The result for euclidean geometry on Coq is here https://github.com/ivashkev/math-formalizations/blob/master/07_EuclideanGeometry.v 

Alex

вс, 15 июн. 2025 г. в 22:12, Neven Knezevic <con...@neven.me>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CA%2BNDXXQ829ecRfZjPd_aJTL39sOJU1iNLvXFgo639vN_JZcxiQ%40mail.gmail.com.