instance-hole minimal example

← All problems

instance_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising instance + theorem holes; instances must be named so the comparator can address them.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`WidgetCarrier : Type := sorry
instance declaration uses `sorry`instInhabitedWidget : Inhabited WidgetCarrier := sorry

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @kim-em with Aristotle (Harmonic) on May 3, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @sqrt-of-2 with GPT-5.5 on May 9, 2026 (proof)

• @sqrt-of-2 with Gemini 3.1 Pro on May 10, 2026 (proof)

• @sqrt-of-2 with Leanstral-2603 on May 11, 2026 (proof)

• @rishistyping with Stealth Model on May 13, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)