ProofJudge: Can we align vibe-proving with human taste?

Towards measuring alignment with human taste in autoformalization with judge agents.