A fully automatic problem solver with human-style output
This addresses the challenge of automating mathematical reasoning with human-style output, though it appears incremental as part of a broader project.
The paper tackles the problem of generating human-like solutions to elementary mathematical problems in metric space theory, achieving results that are difficult to distinguish from those written by human mathematicians.
This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. The program is part of a more general project, which we also discuss.