Open foldl opened 8 months ago
If you add the eq2_triangle definition to defs.txt
without adding an extra breakline (\n) at the end you get this:
Traceback (most recent call last):
File "/home/user/anaconda3/envs/alphageo/lib/python3.10/runpy.py", line 196, in _run_module_as_main
return _run_code(code, main_globals, None,
File "/home/user/anaconda3/envs/alphageo/lib/python3.10/runpy.py", line 86, in _run_code
exec(code, run_globals)
File "/mnt/array50tb/projects/alphageometry/alphageometry.py", line 645, in <module>
app.run(main)
File "/home/user/anaconda3/envs/alphageo/lib/python3.10/site-packages/absl/app.py", line 308, in run
_run_main(main, args)
File "/home/user/anaconda3/envs/alphageo/lib/python3.10/site-packages/absl/app.py", line 254, in _run_main
sys.exit(main(argv))
File "/mnt/array50tb/projects/alphageometry/alphageometry.py", line 603, in main
DEFINITIONS = pr.Definition.from_txt_file(_DEFS_FILE.value, to_dict=True)
File "/mnt/array50tb/projects/alphageometry/problem.py", line 304, in from_txt_file
return cls.from_string(lines, to_dict)
File "/mnt/array50tb/projects/alphageometry/problem.py", line 309, in from_string
data = [cls.from_txt('\n'.join(group)) for group in reshape(lines, 6)]
File "/mnt/array50tb/projects/alphageometry/problem.py", line 34, in reshape
assert len(l) % n == 0
AssertionError
When solving that and adding the sketch_eq2_triangle
function to numericals.py
I get the following output which is valid:
==========================
* From theorem premises:
A B C : Points
AB = AC [00]
* Auxiliary Constructions:
: Points
* Proof steps:
001. AB = AC [00] ⇒ ∠ABC = ∠BCA
==========================
My point is that, with the above codes, it can be proved successfully. But, in Fig 1, it is stated that it can't be proved without the auxiliary construction provided by LLM.
There must be something wrong, either my code, or Fig 1.
I have tried the simple problem of Fig. 1, and it can be proved.
Is there anything wrong?
where
eq2_triangle
is defined as: