Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :)

On Wednesday, June 9, 2021 at 4:45:08 PM UTC-4 di.gama wrote: > On Wed, Jun 9, 2021 at 11:21 AM Jon P wrote: > ... > Is it true that any AI system built on metamath will need these same >> foundations? For instance it will need a parser for the database, a >> verifier and also it will need a

Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :)

On Wed, Jun 9, 2021 at 11:21 AM Jon P wrote: > There have been a couple of AI systems, gpt-f > and Holophrasm > , built on metamath whose aim is to > generate proofs. Are there more I’m not aware of? > Not that I know of, at

[Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :)

There have been a couple of AI systems, gpt-f and Holophrasm , built on metamath whose aim is to generate proofs. Are there more I’m not aware of? If I have understood correctly I think how the search process works is as

Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory

Hi Kunhao, As stated by `zncrng`, ( Z/nZ `5 ) is already the ring itself, so you can work within the ring Y = ( Z/nZ `5 ), and with its multiplicative inverse operation I = ( invr ` Y ). The elements of that ring are not exactly the integers, they are equivalence classes, so your final

[Metamath] [Question of Formalization & Proof] Inverse in number theory

Hello all, Currently, I am stuck on formalization some exercise of number theory involving the multiplication inverse in Z/nZ. Like, compute 3^{-1} in Z/5Z, which gives 2 (because 6 mod 5 = 1). It's easy to translate them into the relation of modulo. For example cheating like