autoformalization.yaml

evaluate_function:
  _target_: examples.autoformalization.evaluate.main
  program_path: ???
  results_dir: ???

distributed_job_config:
  _target_: shinka.launch.SlurmCondaJobConfig
  modules:
  - "cuda/12.4"
  - "cudnn/8.9.7"
  - "hpcx/2.20"
  eval_program_path: "shinka/eval_hydra.py"
  conda_env: "shinka"
  time: "01:00:00"
  cpus: 16
  gpus: 1
  mem: "8G"

evo_config:
  task_sys_msg: |
    You are an expert mathematician with a specialization in group theory. You want to prove the following statement:
    
    "Let $H$ be the subgroup generated by two elements $a, b$ of a group $G$. Prove that if $a b=b a$, then $H$ is an abelian group."
    
    Your task is to identify the minimal set of variables and assumptions needed to formalize the proof in Lean 4. You do not have to provide the proof itself. Therefore, your output is expected to look like:
    
    ```lean
    -- Variables
    theorem abelian_group (<Write the variables needed for the proof here>)
    -- Assumptions
    <Write the assumptions needed for the proof here>
    :
    -- Conjecture
    (<Write the proof's conjecture here>)
    :=
    ```
    
    Key components to add:
    1. Introduce all variables you need to complete the proof.
    2. Write all assumptions needed to complete the proof.
    3. Think about a conjecture that reflects the scientific concept you want to prove. 

    Make sure your output is valid Lean 4. Do not leave the conjecture empty `()`. Do **not** finish the proof, you can leave the program up to the `:=` sign. 

  language: "lean"
  init_program_path: "examples/autoformalization/initial.lean"
  job_type: "slurm_conda"

exp_name: "shinka_autoformalization"