AI: OpenThinker by Open Thoughts

[bil...@gmail.com]

There is an open source GitHub site called Open Thoughts with link:

       https://github.com/open-thoughts/open-thoughts

It has a chatbot called OpenThinker free to use (at least for one shot which can be repeated by reloading the web page).

It shows its chain of thought when asked a question. The final answer appears at the end.

I like the showing of its chain of thought.

I asked OpenThinker the following question "How does metamath prove that if P implies Q then P implies that R implies Q?"

It reformulated my question in the metamath language (getting the parentheses right except omitting the outer parentheses which I don't mind).

It came up with the following proof (verified by metamath-lamp):

qed $p |- ( ( ph -> ps ) -> ( ph -> ( ch -> ps ) ) ) $= ( wi ax-1 a1i ax-2 ax-mp ) ABCBDZDZDABDAIDDJABCEFABIGH $.

--- qed -----------------------------------------------------------------------------------------------
 1|     | ax-1  | |- ( ps -> ( ch -> ps ) )
 2| 1   | a1i   | |- ( ph -> ( ps -> ( ch -> ps ) ) )
 3|     | ax-2  | |- ( ( ph -> ( ps -> ( ch -> ps ) ) ) -> ( ( ph -> ps ) -> ( ph -> ( ch -> ps ) ) ) )
 4| 2,3 | ax-mp | |- ( ( ph -> ps ) -> ( ph -> ( ch -> ps ) ) )
-------------------------------------------------------------------------------------------------------

I refreshed the screen and asked a second question: "How does metamath prove that 2 + 2 = 4?"

Very interesting.

Bill Hale