Hilbert (Apple)

A proving framework linking informal reasoning, recursive problem decomposition and formal verification.

• Developer / Organization: Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu and Ke Ye
• Category: Related research systems & hosted services
• Purpose: Bridge informal reasoning and formal theorem proving.
• Key features: Research framework combining informal reasoning, recursive decomposition and formal proof search.
• Availability: Official project or research page; access varies
• License: Not verified in the linked source (source (opens in a new tab))
• Website / Source code: https://machinelearning.apple.com/research/hilbert (opens in a new tab)
• Version: No public software version found in the linked source
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01