3 problems

The conjecture that formalizing more professional mathematics is the rate-limiting step for AI proof assistance
AI proof assistance refers to AI systems that help mathematicians develop and verify formal proofs, potentially by interacting with an interactive theorem prover. Formalization bot…
openFrom papersartificial-intelligence automated-theorem-proving formalization
0 responses
8
The conjecture that AI-assisted mathematical research requires an adversarial theorem-proving process
An adversarial process is a process in which AI-generated mathematical arguments are checked by an independent formal mechanism, such as an interactive theorem prover. Interactive…
openFrom papersartificial-intelligence automated-theorem-proving formalization
0 responses
10
Whether the behavioural special relativity principle implies the body–observer special relativity principle
Let ${{\mathsf{SPR}}}\xspace^+$ denote the behavioural formulation of the special principle of relativity, and let ${{\mathsf{SPR}_{{{\mathit{B}}}\xspace}}}\xspace$ denote the body…
openFrom papersformalization logic special-relativity
0 responses
6

The conjecture that formalizing more professional mathematics is the rate-limiting step for AI proof assistance