Add @[proof_condition] attribute for conditional formal proofs

[williamjblair]

Some solved problems only have formal proofs under an unproven assumption like GRH. This lets the repo record that assumption as a Lean statement instead of leaving it implicit in a declaration name, so the site can tell conditional formal proofs apart from unconditional ones and show what exactly is assumed.

For context on where this comes from: I audit hosted Lean proofs of Erdős problems at https://williamjblair.github.io/erdos-frontier/, picking up where the erdosproblems wiki's AI-contributions page left off when it was frozen on June 30, and the same audit feeds my #3998 statement batches here. It has so far turned up nine problems whose claimed formal proofs are conditional on unproven hypotheses, four of which #print axioms alone would not catch because the assumption rides as a theorem parameter. This attribute gives that information a home in the repo itself.

Following the review discussion, there is no separate attribute: conditional is a modifier on formal_proof, and the assumed hypotheses are stated in the same file (with sorry proofs) and referenced by name:

/-- The unproven hypothesis assumed by the conditional proof below (statement only). -/
@[category research open]
theorem grh : ... := by
  sorry

@[category research solved,
  conditional formal_proof using lean4 at "https://example.com/proof" assuming grh]
theorem a_conditionally_proved_problem : ... := by
  sorry

Behaviour worth knowing:

• names in assuming are resolved against the environment, so an unknown name is an error and hovering one jumps to the statement
• conditional without assuming is an error, as is assuming without conditional
• if a referenced hypothesis later gains a sorry-free proof, the attribute warns that the proof may no longer need to be conditional
• extract_names emits the declaration names under proofConditions (and supports --exclude=proofConditions); the theorem page shows a Conditional badge and an "Assumes" line

I left the existing Artin conditional declarations unannotated for now, since they don't carry a formal_proof link yet.

Tested with lake build FormalConjectures.Util.Attributes.Basic, a scratch file (not committed) covering the one- and two-hypothesis forms plus the three error paths under #guard_msgs, and lake exe extract_names on that file. Also rebuilt Wikipedia.ArtinPrimitiveRootsConjecture.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[Paul-Lez]

Hey! I think this is a nice idea! How about instead modifying the formal_proof attribute to have an optional conditional keyword in front - this would allow us to write e.g. conditional formal_proof ....

[mo271]

in some sense it would also be nice to store exactly what the hypothesis used is, since that should be relatively short, perhaps we could add those statements to the file (with a sorry proof of course) and then add the declaration name to the attribute?!

[williamjblair]

Thanks @Paul-Lez , agreed! conditional is now a modifier on formal_proof itself (with no separate attribute), so it reads @[conditional formal_proof using lean4 at "<link>" assuming grh]. conditional without assuming errors, as does assuming without conditional.

[williamjblair]

@mo271 makes sense to me! assuming takes declaration names, so the hypothesis lives in the file as a statement with a sorry proof and the attribute references it. The idents resolve against the environment (an unknown name errors, hover jumps to the statement), and extract_names would emit the fully qualified names. This is useful as well bc if the hypothesis later gains a sorry-free proof, the attribute warns that the formal proof may no longer need to be conditional.

[williamjblair]

@Paul-Lez @mo271 reworked along the lines you both suggested: conditional is now a modifier on formal_proof, and the assumed hypotheses are declarations in the file, referenced from an assuming clause. Details in the updated description.

Some context on the motivation: the erdosproblems wiki froze its AI-contributions page on June 30, and I have been continuing that tracking at https://williamjblair.github.io/erdos-frontier/ while auditing the hosted Lean proofs I sync for #3998. That audit has so far turned up nine claimed formal proofs that are conditional on unproven hypotheses, four of them invisible to #print axioms because the assumption rides as a theorem parameter. This attribute is meant to give those conditions a first-class home in the repo

Set to active for review now as well

[Paul-Lez]

Could you add a few tests in FormalConjecturesTest? There should already be a file with tests for attributes, so you could just add a few statements that demo the functionalities you've added.

[williamjblair]

Yes, just added. I added the tests in FormalConjecturesTest/Util/Attributes/Basic.lean covering conditional formal_proof usage, multiple assumed hypotheses, recorded proofConditions + the intended errors for conditional without assuming and assuming without conditional.

The tests also caught that the documented @[conditional formal_proof ...] form was not actually parsing as an attribute, so I fixed that parser registration in the same commit.