Proof search: rationale & configurability of env_pool max parallelism

[hlxr89]

Hi! Thanks for the great work on ProofWala 👋
While exploring the proof-search runner, I noticed the env_pool max parallelism is computed as:

max_parallelism = int(0.15625 * os.cpu_count()) # comment: “don’t go beyond 0.6”

This makes the default ~5/32 cores on a 32-core machine, with an implicit ceiling around 60% of CPU. Could you share the rationale for these numbers? Are they tuned to Lean server behavior, Ray scheduling overhead, GPU-bound LLM inference, or memory pressure? I just thought it would have greatly enhance the performance if it allows more parallelism.

Many thanks!

[amit9oct]

Hi,

Thank you for using our framework, the reason for limiting it was we were running our search on shared cluster and didn't want it to impact other jobs running on the shared host.