Modules
Pick what you’re making and Sundial sets it up: a paper in the right format, a way to search the literature, a checker that reads your claims. Click Use and a workspace opens with it inside. Take it out when you’re done.
Checks your work
Checks your work as you write: a proof, a claim, a compile. It says only what it checked.
Lean Blueprint
- A paper and its Lean 4 formalization kept in step. Every theorem links to a Lean declaration, the agent proves against the real compiler, and a status table shows exactly what is verified.
Claim Verifier
- Review a claim and its citations without reducing evidence to a truth badge: source identity and status, exact claim support, citation coverage, and consistency with the wider record.
Lean 4
- A Lean 4 proving workspace. One setup command installs the latest Lean toolchain plus the community lean4-skills pack into the sandbox, and Hello.lean is a one-file example to build on.
Start here
Pick by what you want to do
Write a paper for ICML 2026
- Official style, compiled on open
- Anonymous for review
- Sunny knows the page limit
Keep your paper and its Lean proof in step
- main.tex and Formalization.lean side by side
- Formalize any selected statement
- Lean 4 and Mathlib ready
Check every claim and citation in a draft
- Select a claim, click Verify
- Source identity, support, coverage
- Findings land as comments
Search nine million theorems and cite what you find
- TheoremSearch, zbMATH, arXiv
- No API keys
- Every claim gets a citation
Work on one goal around the clock
- Each turn in a fresh chat
- Hands off to a successor
- You set the ground truth
Fold proteins and query single-cell atlases
- Paperclip, CELLxGENE, Proto, Boltz
- Runs in the sandbox
- Built for re:AGENT
Most used
re:AGENT - End to End Agentic Science (hackathon)
- Skills and tools for the re:AGENT hackathon: Paperclip full-text literature, CZ CELLxGENE Census single-cell data, Proto's 140+ computational-biology tools, and Boltz-2 structure prediction.
Goal loop
- A workspace that works on one goal continuously. Each turn runs in a fresh chat, does one task, logs what it verified, and hands off to a successor. You set the goal and the ground truth.
Lean Blueprint
- A paper and its Lean 4 formalization kept in step. Every theorem links to a Lean declaration, the agent proves against the real compiler, and a status table shows exactly what is verified.
Claim Verifier
- Review a claim and its citations without reducing evidence to a truth badge: source identity and status, exact claim support, citation coverage, and consistency with the wider record.
ICLR 2026
- ICLR 2026 paper on the official conference style, anonymous until you uncomment the final-copy line for camera-ready.
ACL 2026
- ACL 2026 paper on the ACL Rolling Review style in review mode, with the final switch for camera-ready; preprints may stay non-anonymous.
Assistants
Something Sunny does on its own: when you select text, or on a schedule.
Goal loop
- A workspace that works on one goal continuously. Each turn runs in a fresh chat, does one task, logs what it verified, and hands off to a successor. You set the goal and the ground truth.
Skills
Something Sunny knows how to do when you ask, like searching the literature.
re:AGENT - End to End Agentic Science (hackathon)
- Skills and tools for the re:AGENT hackathon: Paperclip full-text literature, CZ CELLxGENE Census single-cell data, Proto's 140+ computational-biology tools, and Boltz-2 structure prediction.
Math Research
- A mathematics literature workspace. Search 9M+ theorem statements, pull citations and BibTeX from zbMATH Open, fetch full text from arXiv, no API keys. Every claim in main.tex gets a citation.
For math
Lean Blueprint
- A paper and its Lean 4 formalization kept in step. Every theorem links to a Lean declaration, the agent proves against the real compiler, and a status table shows exactly what is verified.
Lean 4
- A Lean 4 proving workspace. One setup command installs the latest Lean toolchain plus the community lean4-skills pack into the sandbox, and Hello.lean is a one-file example to build on.
Annals of Mathematics (aomart)
- Official class for the Annals of Mathematics, maintained for the journal on CTAN. Builds on amsart with the Annals front matter, MSC subjects and the aomplain bibliography style.
ClassicThesis
- Andre Miede's ClassicThesis, a restrained Bringhurst-inspired typographic thesis style on KOMA-Script scrreprt, via the classicthesis package from TeX Live.
Electronic Journal of Combinatorics (e-jc)
- Electronic Journal of Combinatorics paper on the official e-jc style, with the journal's theorem environments, MSC line and dateline in place.
Homework / Problem Set
- Problem set layout on the article class with a fancyhdr course header and amsthm problem and solution environments.
For computer science
Lean 4
- A Lean 4 proving workspace. One setup command installs the latest Lean toolchain plus the community lean4-skills pack into the sandbox, and Hello.lean is a one-file example to build on.
ACM CCS 2026
- ACM CCS 2026 paper in acmart sigconf format with anonymous review mode on and the camera-ready options ready to flip.
ACM Conference (sigconf)
- Generic ACM conference proceedings paper, acmart class in sigconf format. Fits KDD, WWW, CIKM, SIGIR, and most ACM proceedings.
ACM SIGPLAN (PLDI / POPL)
- ACM SIGPLAN proceedings paper, acmart class in sigplan format. Fits PLDI, POPL, OOPSLA, ICFP and other SIGPLAN venues.
ACM Transactions on Graphics (acmart, acmtog)
- ACM Transactions on Graphics manuscript in acmart acmtog format, also the SIGGRAPH journal track, with a teaser figure, CCS concepts and the ACM reference format in place.
Cambridge Thesis
- Cambridge PhD thesis based on the CUED template, driven by the vendored PhDThesisPSnPDF class in its simple print mode with Times text.
For physics
AIP Journals (JAP / APL / JCP)
- REVTeX 4.2 in AIP mode for American Institute of Physics journals such as Journal of Applied Physics, Applied Physics Letters, and The Journal of Chemical Physics.
JHEP / JCAP
- Official jheppub package from SISSA Medialab for the Journal of High Energy Physics and JCAP, article class plus the JHEP bibliography style.
Lab Report
- Physics or chemistry lab write-up on the article class with siunitx units, a booktabs data table, and a pgfplots fit figure.
MIT Thesis
- MIT thesis following the MIT Libraries specifications, driven by the mitthesis class from TeX Live.
Optica (OSA) Journals
- Universal optica-article class for Optica Publishing Group (formerly OSA) journals such as Optica, Optics Express, Optics Letters, Applied Optics, and JOSA A/B.
Oxford Thesis (OxThesis)
- Oxford thesis in the popular OxThesis style, driven by the vendored ociamthesis class with chapter-opening quotations and Oxford-format frontmatter.
For biology and medicine
ACS Journals (achemso)
- The achemso class for American Chemical Society journals such as JACS, Journal of Organic Chemistry, and ACS Nano, shipped with TeX Live.
bioRxiv Preprint
- HenriquesLab two-column bioRxiv preprint class, a popular community template for life-science preprints on bioRxiv.
BMC (BioMed Central)
- Official bmcart class for BioMed Central journals such as BMC Biology, BMC Bioinformatics, and Genome Biology, with the bmc-mathphys bibliography style.
Elsevier CAS
- Elsevier's CAS (Complex Article Structures) cas-dc class, the current els-cas-templates generation used by Elsevier journals on the CAS workflow.
Frontiers Journals
- Official FrontiersinHarvard class for Frontiers journals such as Frontiers in Neuroscience, Immunology, and Psychology, using the Harvard author-date reference style.
MICCAI 2026
- MICCAI 2026 paper on Springer's llncs class with running heads, anonymous for review.
For writing and publishing
Book (memoir)
- Book scaffold on the memoir class with half title, title page, chapter style, and an epigraph-opened first chapter.
Grant Proposal
- NSF-style proposal scaffold on the article class with Project Summary, Project Description, References Cited, and Budget Justification sections.
arXiv Preprint
- Single-column preprint in the widely used arxiv.sty look, article class with a clean title block and natbib references.
ClassicThesis
- Andre Miede's ClassicThesis, a restrained Bringhurst-inspired typographic thesis style on KOMA-Script scrreprt, via the classicthesis package from TeX Live.
Clean Thesis
- Ricardo Langner's Clean Thesis, a clean, simple, elegant thesis design on KOMA-Script scrreprt, via the cleanthesis package from TeX Live.
Dissertate (Harvard)
- Jordan Suchow's Dissertate template, a typographically polished dissertation set in EB Garamond, driven by the vendored Dissertate class on xelatex.
Verifier
Checks your work as you write: a proof, a claim, a compile. It says only what it checked.
Template
Files to start from: a paper in the right format, a thesis, a talk.
Skill
Something Sunny knows how to do when you ask, like searching the literature.
Assistant
Something Sunny does on its own: when you select text, or on a schedule.
All three are the same thing underneath: a folder you add to a workspace, take out, or edit. How modules work →