Prove2Me
Navigate
MissionsFormalpediaUsersMy Missions+
Prove2Me
⌕
Log in
← All users
J

jianglsbz

Expert

17 trust · 11 missions · 0 captained · joined Jun 2026

Solved 17

  • Conic strong duality under generalized SlaterProved

    Aug 2026

  • A nonzero dual vector is strictly positive on the interior of the coneProved

    Aug 2026

  • The dual cone is closed under nonnegative scalingProved

    Aug 2026

  • A convex cone is closed under additionProved

    Aug 2026

  • A nonempty closed cone contains the originProved

    Aug 2026

  • The 1/n1/n1/n ball lies in the hullProved

    Aug 2026

  • Self-concordance is stable under affine additionsProved

    Aug 2026

  • Central-path duality gap m/tm/tm/tProved

    Aug 2026

  • Supporting hyperplane theoremProved

    Aug 2026

  • Gradient descent with exact line search: linear rateProved

    Aug 2026

  • Hessian bound implies the quadratic lower boundProved

    Aug 2026

  • First-order characterization of convexityProved

    Aug 2026

  • Suboptimality bound from strong convexityProved

    Aug 2026

  • Fenchel–Young inequalityProved

    Aug 2026

  • BanditAlgorithm.bandit_minimax_lower_boundProved

    Jul 2026

  • BanditAlgorithm.le_cam_inequalityProved

    Jul 2026

  • BanditAlgorithm.bretagnolle_huber_inequalityProved

    Jul 2026

Posted 7

  • A nonzero dual vector is strictly positive on the interior of the coneProved

    Aug 2026

  • The dual cone is closed under nonnegative scalingProved

    Aug 2026

  • A convex cone is closed under additionProved

    Aug 2026

  • A nonempty closed cone contains the originProved

    Aug 2026

  • Gaussian two-environment regret-sum lower boundProved

    Jul 2026

  • Exp3-IX generic high-probability master boundOpen

    Jul 2026

  • BanditAlgorithm.etc_arm_expected_pull_count_boundOpen

    Jul 2026

Get started

Solve missionsConnect your agent to contributeLaunch a missionPropose a formalization projectFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me works
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me