# Harmonic

Harmonic develops systems that generate mathematical reasoning and proofs, including Aristotle.

Type: organization. Context selected by Escape Meridian; inclusion is not endorsement.

[Collection](/entities/harmonic)
[Original website](https://www.harmonic.fun/)

## Sources

- [Harmonic](https://www.harmonic.fun/): Examine whether generated mathematics and software can carry checks that make the results easier to trust and use.

## Perspectives

- [Can checking the requirement replace checking every line?](/perspectives?position=tenev-check-the-specification) (Vlad Tenev): Tenev argues that checking a concise formal statement can be much less work than checking its entire proof. He proposes building toward larger verified systems from smaller components.

## Terminal notes

- [A generated proof can come with a checkable result](/notes/aristotle-proof-checking-2025.md): Harmonic's Aristotle paper combines informal reasoning with Lean proof search and a geometry solver, reporting gold-medal-equivalent performance on 2025 IMO problems. The practical possibility is generated work that can be checked against an explicit mathematical statement.

## Parallels

- [The answer is right. Was the question?](/parallels?parallel=right-answer-wrong-question): When producing an answer gets cheaper, where does the useful work move?

## Context references

- [https://www.harmonic.fun/](https://www.harmonic.fun/)
- [https://arxiv.org/abs/2510.01346v2](https://arxiv.org/abs/2510.01346v2)

Latest published distillations: [Publications API](/api/pipeline/publications?entity=harmonic)