[submission] irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

[daouid]

Submission URL

https://github.com/daouid/lean-eval/tree/submit/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Model

Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus)

How this solution was produced (optional)

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Acknowledgements

• I understand that the lean-eval CI will fetch my submission URL and run comparator on every lakefile.toml whose name matches a benchmark problem id.
• I understand that only the set of solved problem IDs, along with the metadata I entered above, will be published to the public leaderboard results store.

[github-actions]

Submission result

✅ Newly-solved problems: two_plus_two, ci_regenerate_main_check, list_append_singleton_length, pi1_circle_mulEquiv_int, finite_graph_ramsey_theorem, substInv_X_sub_X_sq_eq_catalan, mulCayley_connected_iff_closure_eq_top, irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius, posSemidef_map_exp, def_hole_example, instance_hole_example, cubic_decay_asymptotic, sturm_separation, dirichlet_eigenvalues_eq_nat_sq, linear_ode_asymptotic_stability, bvp_comparison, heat_kernel_solves_heat_equation, contractibleSpace_houseWithTwoRooms

Attempted 18 / 18; succeeded on 18.

Per-problem

• two_plus_two: pass
• ci_regenerate_main_check: pass
• list_append_singleton_length: pass
• pi1_circle_mulEquiv_int: pass
• finite_graph_ramsey_theorem: pass
• substInv_X_sub_X_sq_eq_catalan: pass
• mulCayley_connected_iff_closure_eq_top: pass
• irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius: pass
• posSemidef_map_exp: pass
• def_hole_example: pass
• instance_hole_example: pass
• cubic_decay_asymptotic: pass
• sturm_separation: pass
• dirichlet_eigenvalues_eq_nat_sq: pass
• linear_ode_asymptotic_stability: pass
• bvp_comparison: pass
• heat_kernel_solves_heat_equation: pass
• contractibleSpace_houseWithTwoRooms: pass