Recording undigested but formalized solutions

[plby]

There are currently many proof claims on https://www.erdosproblems.com/ that are

• correct,
• formalized, and
• undigested.

At https://www.erdosproblems.com/forum/thread/AI%20Contributions#post-5735 Terry suggests that digestion be a requirement to mark a problem as "solved". While I think that this "digested" status is meaningful, I would like to propose that correct formalizations still be recorded. I see two options:

1. Allow a status like proved (Lean) (which is the normal status we've been using) to represent a formalized-but-undigested proof. I have submitted such a PR here: 469 -> proved (Lean) #345
2. Re-work the data representation in problems.yaml to separate the concepts of digested and formalized.

Thoughts?