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
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/9f976d11-d385-402a-858a-70d34ff68557n%40googlegroups.com.
