The Justin Sun Prize focuses on fully solving classic mathematical problems and fully verifying them in Lean. The following Q&A outlines the Prize's mission, verification and evaluation mechanisms, public challenge procedures, application process, and payout arrangements. For specific procedures, please read this document alongside the Justin Sun Prize Selection Rules, the Prize Claim Guidelines, and the latest Participation and Claiming Process.
This FAQ is provided for informational purposes only. Official rights, obligations, and final interpretations are strictly governed by the official Justin Sun Prize Selection Rules and the Terms of Use published on our website.
I. Mission and Participation
Q1. Why was the Justin Sun Prize established?
Mr. Justin Sun established the Prize to give back to the mathematical research that underpinned his career, providing sustained support for mathematical breakthroughs and their formal verification. As he shared in his open letter: "Wealth comes from mathematics, and to mathematics it should return."
The Prize recognizes not only breakthroughs in solving mathematical problems, but also the work of translating these achievements into machine-verifiable formats. By separately acknowledging and rewarding both types of contributions, the Justin Sun Prize aims to provide timely recognition for traditional research and achievements built through human-AI collaboration.
Q2. What specific achievements does the Prize reward, and how does it differ from traditional awards?
Currently focused on mathematics, the Prize is based on a public Problem List that recognizes both problem solvers and Lean formalizers. The former solves the mathematical propositions, while the latter converts those solutions into machine-verifiable formal proofs.
Unlike traditional awards that honor individuals annually based on their broader careers, this Prize rewards verifiable solutions to specific problems. Under current participation procedures, only complete solutions to original benchmark problems and complete Lean proofs are eligible. Special cases, intermediate lemmas, weaker conclusions, conditional arguments relying on unproven extra assumptions, and Lean proofs that use sorry, admit, or newly added unproven assumptions to fill missing steps are strictly excluded. Submission, acceptance, or Pull Request (PR) merging does not in itself constitute an award.
Q3. What is the eligible timeframe for submissions, and are prizes awarded immediately upon completion?
The Prize sets a cutoff date for retroactive financial awards. Under the Selection Rules, historical achievements eligible for prizes are retroactively covered starting from January 1, 2026.
This cutoff date applies solely to financial eligibility. Mathematical achievements completed prior to January 1, 2026, will still be documented along with their contributors, but will not receive retroactive cash prizes. However, if a mathematical solution was completed before this date, but its corresponding Lean formalization is completed after January 1, 2026, and meets all requirements, the Lean formalization remains eligible for evaluation. Problem-solving and Lean formalization contributions are evaluated independently; an earlier completion date for one does not disqualify an otherwise eligible contribution for the other.
Meeting the timeframe requirement does not mean a payout is issued immediately upon completion. Participants must complete submission and verification in accordance with the latest Participation and Claiming Process. Once a contribution enters candidacy, it must undergo a 14-day public notice period, identity verification, an individual claim application, written confirmation by the awardee, and pre-announcement review. If a valid challenge is raised during the public notice period, it must be verified and resolved. Submission, acceptance, PR merging, or the expiration of the public notice period does not independently constitute an official award conferral.
The Prize Operator will arrange prize disbursements once all applicable procedures are finalized and the recipient is officially listed. Corresponding physical certifications and medals (where applicable) will be shipped in accordance with official award notices.
Q4. Who funds the Prize, and how are payouts issued?
The Prize is funded personally by Mr. Justin Sun and disbursed by the Prize Operator. It operates as a non-profit, philanthropic initiative.
Recipients must claim their prize in cryptocurrency. Payouts are distributed via TRC-20 USDT or ERC-20 USDC transfers, provided the recipient meets all standard receiving conditions and compliance requirements.
Q5. Who can participate? Who claims the prize when AI is involved?
The Prize is open to all eligible individuals and teams without restrictions on nationality, institutional affiliation, or background. Professional researchers, independent enthusiasts, and human-AI collaborative teams may all submit their work. Formal publication is not a prerequisite, but submissions must provide complete mathematical solutions and complete Lean proofs for the original problem. Problem solvers may submit mathematical solution details without providing a Lean repository. However, Lean formalizers (or those fulfilling both roles) must submit a reproducible Lean formalization source and verification metadata following the official PR template. Each contributor must personally initiate their own prize claim.
For achievements produced with the participation of AI systems, the declaring applicant, authorized representative, and prize recipient are determined in accordance with the Selection Rules. The prize recipient must be a natural person, legal entity, or other lawful organization capable of meeting applicable legal requirements.
II. Verification, Evaluation, and Priority Determination
Q6. Who oversees the evaluation process? Can AI independently decide the winners?
Verification follows a strict sequence: the Organizing Committee first verifies the mathematical solution and registers the problem-solving candidate, then validates the corresponding Lean formalization and registers the formalization candidate. Formalizers must submit a reproducible proof repository pinned to a specific commit hash, after which the Committee independently verifies the problem statement and reproduces the proof. AI or automated tools may participate in analysis and verification, but do not independently dictate award decisions.
AI-generated evaluations serve strictly as supporting references and do not independently determine an award. The Organizing Committee makes final evaluation decisions in accordance with the Selection Rules and retains authority over all award approvals.
Committee members with a conflict of interest regarding a candidate must recuse themselves. Any re-examinations are conducted by members uninvolved in the original review.
Q7. Does Justin Sun personally have the final say on award decisions?
Mr. Justin Sun, as founder and funder, sets the Prize's strategic direction, Problem List, and budget. However, he does not participate in academic evaluations, including award selections, achievement tiering, or priority attribution.
Q8. Why use machine verification rather than relying solely on peer review?
Machine verification and human scholarly judgment serve distinct purposes. The validity of a mathematical solution is first verified through independently auditable materials like public proofs, publications, or official announcements by the authors or project teams before advancing to Lean formal verification. A Lean proof must be complete and reproducible, and must not rely on sorry, admit, or newly added unproven assumptions to fill missing steps. For formalization submissions, the Committee verifies the pinned commit hash, formal statements, environment dependencies, build commands, and axiom usage. A successful compilation alone does not bypass the requirement to verify the underlying mathematical solution and the fidelity of the formal statement.
The Prize also incorporates human peer review. A problem's historical lifespan, the rigor of human peer review it has undergone, and its broader recognition within the mathematical community are all key metrics for determining the final award tier and prize amount. While formalizations in other proof systems may serve as references, they cannot replace required Lean verification. Finally, journal peer review evaluates the underlying mathematical proof, not the Lean code. Therefore, a paper published in a peer-reviewed journal does not automatically mean its Lean formalization is verified.
Q9. How is priority determined to recognize the "first" to solve a problem?
The Prize distinguishes between two types of contributions: problem-solving and formalization. The solver is the first individual or team to solve the mathematical proposition, while the Lean formalizer is the first to complete the formalization. Priority for each is determined independently and cannot be cross-referenced. Prior publication of a mathematical proof does not presume prior formalization, and vice versa.
Problem-solving and formalization are distinct roles, each maintaining separate candidacy and public notice records. A mathematical solution may be registered as a candidate using public evidence provided by the solver, the formalizer, or a third party; however, registration does not constitute a prize claim. Claims must be personally initiated by the respective contributor. Formalization candidacy is anchored by the verified proof repository and the specified commit hash.
Priority for Lean formalization is determined primarily by the timestamp of the specified commit hash in the applicant's repository, combined with independently verifiable public history that ties that proof version to the claimed date (e.g., public repository history, public releases, third-party archives). Because Git commit timestamps can be user-specified, they cannot serve as sole proof of completion; conflicting or uncorroborated timestamps must be reconciled to establish a reliable time anchor.
Once a contribution PR is merged, the corresponding role enters a 14-day public notice period. Problem-solving and formalization roles are timed independently without waiting for each other. PR merging simply records the contribution and does not constitute an award conferral; the expiration of the public notice period alone is also insufficient to disburse a prize. Official award distribution occurs only after the public notice period expires with no unresolved challenges, pending reviews for the same role are completed, and written confirmation from the recipient is received.
During the public notice period, formal challenges regarding mathematical correctness, attribution, priority, identity, or prize eligibility may be submitted via the official Formal Dispute Issue form. Routine record corrections should be submitted via Correction Issue forms and do not trigger the challenge workflow.
III. Application and Prize Claiming
Q10. How do I participate in verification, apply for an award, and claim a prize?
The latest process spans three stages: submission & verification, award claiming & public challenge, and prize disbursement. Submission, acceptance, and PR merges do not constitute formal award confirmation.
Stage 1: Submission & Verification — Select a problem from the official Problem List, fork the official repo, and submit a PR matching your contribution type. Problem Solvers only: Select Mathematical solver information to provide a complete mathematical proof or publication link alongside proof of authorship, with no Lean repository required.Lean Formalizers (or those fulfilling both roles): Submit your own Lean proof repository, a pinned 40-character commit SHA, formal statements, environment dependencies, and build verification metadata. The Organizing Committee will first confirm whether the underlying mathematical solution exists before conducting Lean verification. Merging a contribution PR places it on the public notice table for a 14-day public notice period, but merging alone does not constitute an award conferral.
Stage 2: Award Claiming & Public Challenge — Once a contribution is accepted, the contributor must personally open an [Award claim] issue using the claim-award form via their personal GitHub account, specifying a contact email in the Follow-up contact email field. This email will be displayed in the public issue, eliminating the need to post follow-up comments. The issue uses the GitHub handle solely as an identifier; real names, institutional affiliations, or private details do not need to be disclosed publicly. Next, send an identity verification email from that follow-up email address to thejustinsunprize@hejustinsun.com, linking the claim issue to the merged PR. Identity verification is mandatory for problem-solving claims; pure Lean claims may forgo independent verification if source code attribution reliably links the GitHub account to the author. Formal disputes may be raised during the public notice period in accordance with the rules.
Stage 3: Award Disbursement — Upon expiration of the public notice period with no unresolved challenges or pending reviews under the same identity, written confirmation from the recipient is required. Only then may payout networks, addresses, and mailing details be provided to finalize entry onto the official award list and trigger the disbursement workflow.
Sensitive identity documents, real names, institutional affiliations, payment networks, wallet addresses, and mailing addresses are handled exclusively via official email and must never be posted in GitHub issues. The sole official contact email is thejustinsunprize@hejustinsun.com. Official communications will originate exclusively from @hejustinsun.com domains, and the team will never ask for wallet private keys or seed phrases.
Q11. How is the prize amount determined? How is it split between the problem solver and the Lean formalizer?
Prizes are structured into five tiers: Pinnacle, Breakthrough, Landmark, Advance, and Contribution. The Pinnacle tier awards $1,000,000, while prizes for the other tiers are detailed in their respective award announcements. Submissions are evaluated against three criteria—durability, journal or conference ranking, and peer review status—with final adjustments applied based on the degree of completion.
Under the Justin Sun Prize Selection Rules, 70% of a problem's total prize fund is allocated to the problem solver and 30% to the Lean formalizer; if an entity fulfills both roles, it receives the full prize amount. Teams must designate an authorized representative and a lawful payee, and the Organizing Committee will not intervene in internal team allocations.
The Organizing Committee will continuously optimize problem parameters and reward standards for future additions based on operational experience. Any rule adjustments will be publicly released through version updates and take effect upon publication; prize arrangements for previously published problems and confirmed awards will remain unaffected.
Beyond financial awards, physical certificates, medals, or other commemorative items may be provided depending on specific award arrangements. These commemorative arrangements are separate from the prize allocation rules; their specific format, eligible recipients, quantity, and distribution methods are governed by official award notices and remain subject to adjustment based on operational needs. Any such adjustments will not affect confirmed prize evaluations or disbursements.
Q12. Will all problems be solved and rewards issued immediately going forward?
The Prize does not rely on fixed annual cycles or award ceremonies; however, "immediate issuance upon resolution" does not mean that any self-proclaimed solution can instantly receive a payout. The current workflow accepts only complete mathematical solutions and complete Lean proofs, progressing through a strict sequence: solution confirmation, Lean verification, PR merging, a 14-day public notice period, necessary challenge handling and re-examination, written confirmation from the recipient, official award announcement, and claim procedures.
Q13. How are false claims prevented? Can prizes be claimed based solely on public attribution or online usernames?
Prize claims must be initiated personally by the contributor using their own GitHub account to post a claim issue. The issue may use the GitHub handle solely as a public identifier without disclosing real names; real names, institutional affiliations, and other private information are verified via email. Teams, AI-assisted achievements, and actual payees must still complete applicable identity, authorization, and compliance verifications under the Selection Rules. Public attributions, online handles, model names, or wallet addresses alone are insufficient for official award conferral and payee confirmation.
The Follow-up contact email in the claim issue form serves as the primary communication channel and is displayed publicly. Claimants must email the official team from this address to link their claim issue to the merged PR. Problem-solving claims (including those fulfilling both roles) must complete independent identity verification; pure Lean claims may forgo separate verification if source code attribution already reliably establishes the link between the account and the author. Acceptable verification methods include paper author emails, established institutional or author websites, historical signing keys, or other independently verifiable means, and claimants must respond to verification requests initiated by the Organizing Committee. Non-public information such as ID documents, payout addresses, and mailing addresses must not be posted in GitHub issues.
Q14. How are prizes claimed and allocated when awarded to teams or multiple co-recipients? Can a project lead collect the entire prize on behalf of the team?
Teams must designate an authorized representative and a lawful payee, providing valid documentation to verify their authorization. Being a corresponding author, project lead, or PR submitter does not automatically grant an individual the right to claim the entire prize on the team's behalf. The Organizing Committee does not participate in internal prize allocations. If a prize is to be split among multiple recipients, all co-recipients must jointly submit a legally binding written document on prize allocation and receipt confirmation. This document must explicitly detail each recipient party, their allocation percentage or amount, and corresponding payment arrangements, validly signed or confirmed by all relevant parties. Disbursements will be processed by the Organizing Committee in accordance with verified award outcomes and submitted documentation. Should any dispute arise regarding allocation or authorization, the corresponding disbursement may be temporarily withheld.
Commemorative arrangements (such as physical certificates or medals) are independent of internal prize allocations. For team awards, the eligible recipients, quantity, and delivery of physical items will be determined by the Organizing Committee and detailed in the official award notices.
Q15. Are prize disbursements subject to taxation? Will the Prize Operator withhold tax?
The tax treatment of prize funds depends on applicable laws and the recipient's specific tax status. Recipients are responsible for understanding and fulfilling all applicable tax reporting and payment obligations. If legally required, the Prize Operator will withhold applicable taxes in accordance with regulations and provide corresponding tax documentation. The Prize Operator does not guarantee general tax exemptions or specific post-tax net payout amounts.
Q16. Who bears the on-chain transaction fees incurred during prize disbursements?
The Prize Operator will cover all network transaction fees incurred during prize disbursements via the TRON or Ethereum networks.
Q17. How is the payee confirmed for achievements involving AI? Can prizes be claimed merely by providing a model name or wallet address?
No. Submitting an AI model name or a wallet address alone is insufficient. The applicant party, authorized representative, and lawful payee arrangements must comply with the Selection Rules. These procedures must be completed by natural persons, legal entities, or their representatives authorized in writing, who have passed full KYC checks. Providing only the name of an AI system or a wallet address is not sufficient to confirm the payee.
Q18. What should be done if names on academic records and identity documents do not match?
If name discrepancies between academic records and identity documents stem from Chinese-English spelling differences, name order variations, former names, or legal name changes, please provide a written explanation and supporting documentation. Name discrepancies of the same individual and third-party payment collection represent distinct categories and will be verified and processed separately.
Q19. Do award recipients have to collect their prizes in person, or can a third party or institution collect on their behalf under special circumstances?
As a rule, individual recipients must collect their prizes in person. For team awards, an authorized representative and lawful payee must be designated in accordance with the Selection Rules; where achievements are generated by AI systems, the applicant entity, authorized representative, and lawful payee must likewise be determined pursuant to the Selection Rules.
Aside from these scenarios, third-party collection is not permitted under standard procedures. If special circumstances genuinely prevent self-collection, an application for an exception must be submitted. Upon approval, the awardee must provide a handwritten authorization document, identity documentation for both parties, and proof of relationship; the third-party payee must also complete corresponding identity and compliance verifications. If the collector is a corporate entity, trust, fund, or other organization, the corresponding entity's credentials and authorization documents must be provided.
If the original payment method fails and a switch to third-party collection is requested, all relevant payout and authorization materials must be resubmitted and re-reviewed. Third-party collection is strictly a logistical arrangement and does not alter the identity of the original award recipient or the ownership of the prize.
For other special entities or complex scenarios, specific handling requirements will be determined on a case-by-case basis.
Q20. How can a prize be claimed if the winner is a minor, is deceased, or is otherwise unable to manage the claim?
If the winner is a minor, is deceased, or cannot independently complete the process, their legally authorized guardian or representative must contact the Organizing Committee and provide official credentials and supporting documents. Eligibility and claim procedures will be determined in accordance with applicable laws and the Selection Rules. Note that submitting a proxy application does not automatically establish or transfer prize ownership.
Q21. What if there are payment restrictions concerning the recipient's payout network, recipient address, country, or region? Can alternative payment methods be used?
If compliance or regulatory concerns arise, additional verification may be required, or disbursement may be temporarily suspended. If the recipient needs to change the payout network or recipient address, the request must be submitted via the original official email thread and undergo required verification before payment execution. For payments prohibited under applicable laws, recipients must not attempt to circumvent restrictions by switching currencies, using alternative addresses, or routing funds through third-party intermediaries. Payout network selections and recipient addresses must be submitted exclusively via email; never post them in a GitHub issue.
Q22. What should be done if the prize claim cannot be completed on time, a postponement is required, or the winner wishes to forfeit the prize?
Please explain the situation within the original official email thread. As a rule, submitting supplemental materials, requesting extensions, or adjusting claim arrangements does not require opening a new claim issue. However, if the original candidate has been replaced or their qualifying status has changed, the new contributor must independently submit their own claim issue, complete their own identity verification, and provide their own written confirmation. They may not reuse or inherit any confirmations, payout details, or shipping addresses from the replaced party.
IV. Dispute Handling and Public Oversight
Q23. How are prizes awarded in cases of disputed identity, multiple claimants, cross-platform priority disputes, or unclear attribution?
First, distinguish between identity verification issues and achievement attribution disputes. If identity, authorization, or the legitimate payee has not been verified, applicants must submit supporting documentation; no funds will be released to unconfirmed recipients. Disputes regarding award recipients or achievement attribution must be resolved in accordance with applicable rules before any payments are processed.
When multiple parties claim the same achievement, a distinction must be made between team collaborations and independent work. For team-based achievements, the award is granted to the team as a whole, and the Organizing Committee will not intervene in internal prize allocation.
For achievements completed independently by different parties, recipients will be determined based on the Selection Rules and the latest participation guidelines, supported by verifiable records and timestamps. Priority for Lean formalization is, in principle, evaluated by comparing the commit timestamps in the candidate's repository alongside independently verifiable public history; a Git commit date alone is insufficient to establish completion time. The submission time of a claim issue, the delivery time of a claim email, or internal processing speeds do not alter established priority.
During the 14-day public notice period preceding the formal award, anyone may challenge the mathematical correctness, attribution, priority, identity, or prize eligibility by submitting via the official Formal Dispute Issue form. Routine record corrections should be handled via Correction Issue forms instead. If a challenge arises during the public notice period, the review period will not close until that challenge is fully resolved. Disputes, re-evaluations, and revocations occurring after the formal award will continue to be governed by the Selection Rules.
Q24. How is prize money handled when objections are raised regarding award results, or when payment identity, authorization, attribution, or amount is unverified?
Prior to the formal award, payouts will not proceed if any unresolved public challenges, pending submissions under the same identity, eligibility/identity challenges, or missing written award confirmations remain for the relevant participant. Post-award disputes, revocations, and clawbacks of disbursed funds remain subject to the Selection Rules.
Q25. What happens if issues with an award-winning proof or determination are discovered after the prize has been awarded?
Awardees or any third party may file an objection within 14 days of public disclosure regarding tier classification, credit attribution, formal verification conclusions, awardee designation, or related matters. Objections must be reviewed by Organizing Committee members who did not participate in the original evaluation, with final conclusions published upon consensus approval.
Revocation may be triggered by any of the following conditions: defects in proposition fidelity, failure to detect placeholder or unreviewed axioms, erroneous definitions yielding vacuous conclusions, disclosed soundness vulnerabilities in the underlying proof system or checker that compromise verification, refutation of the mathematical result by peer review, erroneous awardee designation, voluntary disclosure by the awardee, or other material grounds.
An awarded tier may be revoked upon consensus approval by the Committee members who participated in the review, subject to public disclosure of the rationale and complete evidence. In principle, disbursed prize funds are not subject to clawback. The revocation record will be permanently displayed alongside the original award entry.
Objections cannot pertain to whether the problem itself has been solved, as that determination rests exclusively with the broader mathematical community.
For prizes obtained through fraud, impersonation, plagiarism, intentional submission of false documentation, or other severe violations of the Selection Rules, the Prize Operator reserves the right to demand full repayment and pursue other legal remedies.
Q26. How does the public oversee award results and prize disbursements? Will recipients' personal information be disclosed?
The Problem List, contribution PRs, candidate notices, and award records are published on GitHub. Claim issues are publicly visible, including the Follow-up contact email; legal names and institutional affiliations do not need to be disclosed within the issue. Cryptocurrency payments can be publicly verifiable via on-chain transaction records.
Applicants must ensure that all materials submitted for verification are free of intellectual property defects and do not infringe upon third-party rights. Sensitive identity documents, payout networks, recipient wallet addresses, mailing addresses, and other non-public personal data must be submitted strictly via the official email address—never in a GitHub issue. The Prize Operator processes personal information in compliance with applicable laws, using it solely for identity verification, award confirmation, prize claiming, and fund disbursement.