Check if this is the main process (rank 0) in distributed training

Generate conjectures from seed theorems and proofs Args: conjectures_per_statement: Number of conjectures to generate per statement

Finetune a local model on a dataset. Args: model_save_path: Path to save the finetuned model train_data: List of tuples of (

Runtime check that each optimizer step contains *complete groups* globally. This is written to be safe even when `dataloader_drop_last=False`, i.

This will clean up all the workers that the server launched. Important incase there are pending workers that never have to be used.

Launches a worker as a subprocess on the master machine.

Prepare the train data for the conjecturer This is easier than preparing the prover dataset as we simply train on all of the conjectures

Prepare the train data for the prover Args: prover_dataset_path: Path to dataset we use to train the prover so far iteration

Review the conjectures

Note that launching master workers will occur for query server equal to number of GPUs on master machine.

From https://github.com/project-numina/kimina-lean-server/blob/main/server/split.py Splits a code snippet into a header (imports) and body.