[Feature Request] Mutli-file challenge support

I have a couple of Lean projects where the sorries live across multiple files, but comparator today only takes one challenge and solution file.

One example that works well enough today, but is a tad bit clunky, is to import them all into a single file, similar to a module export file.

-- challenge.lean
import Challenge.FileA
import Challenge.FileB

-- config.json
{
    "challenge_module": "Challenge",
    "solution_module": "Solution",
    "theorem_names": ["comm", "assoc"],
    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
    "enable_nanoda": false
}

Alternatively, lean4export supports multiple outputs, so comparator could directly allow specifying multiple challenges and solutions:

-- config.json
{
    "challenge_modules": ["ChallengeA", "ChallengeB"],
    "solution_modules": ["SolutionA", "SolutionB"],
    "theorem_names": ["comm", "assoc"],
    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
    "enable_nanoda": false
}

Or do it as a dictionary pair, if one is worried about making sure the challenge and solution line up.

I have a vibed up draft here for that - https://github.com/leanprover/comparator/compare/master...rusch95:comparator:multi-module-checks - for checking that it's a straightforward enough change, though I think there's a couple of edge cases to do it safely.

Thoughts?

Start with the config.json examples and the linked multi-module-checks draft, then inspect how comparator currently handles challenge_module and solution_module. Clarify the supported multi-file configuration and its challenge/solution pairing, including the edge cases mentioned in the issue; done means multi-file Lean projects can be checked while theorem_names, permitted_axioms, and enable_nanoda continue to work.