search

openai / miniF2F

Formal to Formal Mathematics Benchmark
293 stars 42 forks source link

FOL/SMT classical tools support? #122

Open brando90 opened 1 year ago

brando90 commented 1 year ago

I know Lean is a higher order logic...but it would be nice to have a benchmark where classical SMT methods can be benchmarked too. What is the possibility/effort/path to translate miniF2F to a format compatible with classical SMT/ATP solvers?

DyeKuu commented 1 year ago

Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them?

brando90 commented 1 year ago

Of course!

CVC5, Vampire, Z3 and I bet many more! I don't know what format of theorems they take but I'm guessing they are FOL. I hope to find out more and help with this issue eventually :)

Get Outlook for Androidhttps://aka.ms/AAb9ysg

From: Kunhao ZHENG @.> Sent: Tuesday, November 1, 2022 8:18:44 PM To: openai/miniF2F @.> Cc: Brando Miranda @.>; Author @.> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122)

Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them?

— Reply to this email directly, view it on GitHubhttps://github.com/openai/miniF2F/issues/122#issuecomment-1299509640, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAOE6LWS4Z7D4BRXN3QHQ5DWGHMRJANCNFSM6AAAAAARTXFK4M. You are receiving this because you authored the thread.Message ID: @.***>

brando90 commented 1 year ago

If you run Isabelle's sledgehammer or coqhammer they usually say which atp they are running in your current open goals.

Get Outlook for Androidhttps://aka.ms/AAb9ysg

From: Brando Miranda @.> Sent: Tuesday, November 1, 2022 10:25:47 PM To: openai/miniF2F @.>; openai/miniF2F @.> Cc: Author @.> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122)

Of course!

CVC5, Vampire, Z3 and I bet many more! I don't know what format of theorems they take but I'm guessing they are FOL. I hope to find out more and help with this issue eventually :)

Get Outlook for Androidhttps://aka.ms/AAb9ysg

From: Kunhao ZHENG @.> Sent: Tuesday, November 1, 2022 8:18:44 PM To: openai/miniF2F @.> Cc: Brando Miranda @.>; Author @.> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122)

Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them?

— Reply to this email directly, view it on GitHubhttps://github.com/openai/miniF2F/issues/122#issuecomment-1299509640, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAOE6LWS4Z7D4BRXN3QHQ5DWGHMRJANCNFSM6AAAAAARTXFK4M. You are receiving this because you authored the thread.Message ID: @.***>

DyeKuu commented 1 year ago

as far as i know there is no undergoing efforts on porting minif2f to these solvers. would like to know if this is in principle feasible?

brando90 commented 1 year ago

Would love to know if this is feasible for sue. Do you know? I will ask my circle of connections.

Get Outlook for Androidhttps://aka.ms/AAb9ysg

From: Kunhao ZHENG @.> Sent: Wednesday, November 2, 2022 7:02:47 PM To: openai/miniF2F @.> Cc: Brando Miranda @.>; Author @.> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122)

as far as i know there is no undergoing efforts on porting minif2f to these solvers. would like to know if this is in principle feasible?

— Reply to this email directly, view it on GitHubhttps://github.com/openai/miniF2F/issues/122#issuecomment-1301562411, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAOE6LV3LHVQJCQF3GCALXDWGMMMPANCNFSM6AAAAAARTXFK4M. You are receiving this because you authored the thread.Message ID: @.***>