On Wed, Sep 9, 2020 at 5:58 PM Norman Megill wrote:
> On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote:
>
>> Norm:
>>
>> Thanks for the reply, I’m definitely going to hang out around here more
>> often. The 100 theorems is my ideal option, I was scheming the list
>> provided and
On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote:
> Norm:
>
> Thanks for the reply, I’m definitely going to hang out around here more
> often. The 100 theorems is my ideal option, I was scheming the list
> provided and some theorems caught my eye, like the four colors one,
>
> 1) Maybe you mention it in the article and I missed it, but why is the model
> called "GPT-f"? Does 'f' stand for "formal"?
Exactly
> 2) Have you tried augmenting the set.mm database by adding theorems with
> renamed variables (like a version of id with |- ( ps -> ps ) instead of |- (
> ph
Nice work! I really hope that a publication from such a credible AI company
will bring more attention to metamath.
I have several small questions, hope you could shed some light on some of
them.
1) Maybe you mention it in the article and I missed it, but why is the
model called "GPT-f"? Does
> This seems to me to be a remarkable claim, especially since creating formal
> proofs is something that even relatively early computers were doing. There
> are many other automated provers. Coq proved the 4-color theorem, and prover9
> found a previously unknown algebraic proof.
The claim is
On September 9, 2020 4:46:47 AM EDT, 'Stanislas Polu' via Metamath
wrote:
>Hi!
>
>We finally released a paper describing our methodology for the proof
>assistant.
>
>It's available on arXiv here: https://arxiv.org/abs/2009.03393
>
>Any feedback/suggestions or questions is obviously welcome!
>
Hi! and thanks for all the replies, I definitely wasn't expecting so many!
I will address all of your kind replies:
Norm:
Thanks for the reply, I’m definitely going to hang out around here more
often. The 100 theorems is my ideal option, I was scheming the list
provided and some theorems
Thanks Mario!
I will dig in that direction and hopefully will make a PR for gsumwsN
and amgmN for N=3..8 \o/
-stan
On Wed, Sep 9, 2020 at 4:12 AM Mario Carneiro wrote:
>
>
> On Tue, Sep 8, 2020 at 3:46 PM 'Stanislas Polu' via Metamath
> wrote:
>>
>> I was expecting to find something along
Hi!
We finally released a paper describing our methodology for the proof assistant.
It's available on arXiv here: https://arxiv.org/abs/2009.03393
Any feedback/suggestions or questions is obviously welcome!
Special shout out to David Wheeler and Mario Carneiro in the
acknowledgements that I
