How Andrew HSC verifies worked solutions

A verified solution carries exactly one of these labels, and the label's hover text says what it means.

• Verified · CAS — "This solution has been checked by a computer algebra system (CAS)."
• Verified · Lean 4 — "This solution has been formally verified with the Lean 4 proof checker."
• Verified — "This solution has been reviewed and verified." Normally a teacher's or staff review.

Where more than one check applies, the label shows the strongest: Lean 4 if the proof checker accepted the solution, otherwise CAS if the algebra check passed, otherwise the plain label for a human review. A solution that none of the checks has passed carries no label, and the public sample questions on this site show the same label a teacher sees in the product, never a stronger one.

The CAS check runs SymPy, an open-source computer algebra system. Where the question is one it can re-solve — a derivative, an integral, an equation, a probability, a financial formula or a series — SymPy re-derives the answer from the question and compares it with the solution's final answer. For other solutions it checks that the equalities written in the solution hold. Both checks earn the same Verified · CAS label. The check is deterministic and involves no AI, so a pass means the mathematics closes, not that a model agreed with itself.

Not every question can be re-derived. A proof, a question that depends on a diagram, or a "show that" with no single closing value gives a CAS nothing to recompute, and those solutions are never labelled by this check. That is why the product's own wording is CAS-verified solutions where available, and never a claim about the bank as a whole.

For a stricter check, a solution's LaTeX is translated by a language model into Lean 4, the proof assistant, using its Mathlib library, and the translation is sent to a hosted Lean checker that compiles it. A solution earns "Verified · Lean 4" only when the Lean code compiles with no gaps; a rejection or a failed translation is recorded as such and the solution keeps whatever other label it has. A failed attempt goes through a bounded repair loop in which the model reads the compiler's errors and tries again, and some topics, among them proofs, vectors and mechanics, are routed around the checker because they cannot be translated reliably and so never earn the label.

The automated checks sit inside a review pipeline with people at both ends: AI generates, CAS verification runs, admins review, teachers flag issues and admins resolve them. The plain "Verified" label is the mark of that human review. Any teacher can flag a question from the bank view, and a rejection is tied to the exact solution text that was reviewed, so if the solution is later edited the earlier verdict no longer applies and the question goes back for another look.

Plainly: not every question in the bank has been checked by any of the three methods, and Andrew HSC does not pretend otherwise. The signal is the absence of the label. There is no "unverified" badge on a student's screen, by design, because a correct but unchecked solution should not be read as wrong; the label is simply not there.

• In the question bank, the Verification filter offers All Questions, Verified and Unverified, so a worksheet or an exam can be built from checked solutions only.
• On a question card, the label sits beside the topic and mark value, and the hover text repeats the sentence quoted above for that label.
• Staff see an additional "Review" marker on questions awaiting review; teachers and students do not.
• The sample questions on this site's public pages, such as the worksheet generator page, carry the same labels, drawn from the same fields.

A label says that a particular check passed on a particular solution text. It does not say that the question suits your class, that the marks match your school's scheme, or that the method is the one you taught. The Terms of Use put it directly: content generated by AI may contain errors; while Andrew HSC employs CAS verification and review processes, it does not guarantee the mathematical accuracy of all generated questions or solutions, and teachers are responsible for reviewing AI-generated content before use in formal assessments.

Teachers remain responsible for reviewing AI-generated content, including worked solutions, before using it in formal assessments.

That responsibility is why the labels exist at all. A teacher building a school's shared bank can tell at a glance which solutions a machine or a colleague has already stood behind, and spend their own checking time where it is still needed. See pricing for the plans that include the bank and its verification labels.