Skip to content
Navigation Menu
Sign in
Appearance settings
Platform
AI CODE CREATION
GitHub Copilot
Write better code with AI
GitHub Copilot app
Direct agents from issue to merge
MCP Registry
Integrate external tools
DEVELOPER WORKFLOWS
Actions
Automate any workflow
Codespaces
Instant dev environments
Issues
Plan and track work
Code Review
Manage code changes
Code Quality
Enforce quality at merge
APPLICATION SECURITY
GitHub Advanced Security
Find and fix vulnerabilities
Code security
Secure your code as you build
Secret protection
Stop leaks before they start
EXPLORE
Why GitHub
Documentation
Blog
Changelog
Marketplace
View all features
Solutions
BY COMPANY SIZE
Enterprises
Small and medium teams
Startups
Nonprofits
BY USE CASE
App Modernization
DevSecOps
DevOps
CI/CD
View all use cases
BY INDUSTRY
Healthcare
Financial services
Manufacturing
Government
View all industries
View all solutions
Resources
EXPLORE BY TOPIC
AI
Software Development
DevOps
Security
View all topics
EXPLORE BY TYPE
Customer stories
Events & webinars
Ebooks & reports
Business insights
GitHub Skills
SUPPORT & SERVICES
Documentation
Customer support
Community forum
Trust center
Partners
View all resources
Open Source
COMMUNITY
GitHub Sponsors
Fund open source developers
PROGRAMS
Security Lab
Maintainer Community
GitHub Stars
Archive Program
REPOSITORIES
Topics
Trending
Collections
Enterprise
ENTERPRISE SOLUTIONS
Enterprise platform
AI-powered developer platform
AVAILABLE ADD-ONS
GitHub Advanced Security
Enterprise-grade security features
Copilot for Business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Pricing
Search
/
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
leanprover
/
lean-eval
Public
Notifications
You must be signed in to change notification settings
Fork
40
Star
47
Code
Issues
11
Pull requests
15
Actions
Projects
Security and quality
0
Insights
Additional navigation options
Code
Issues
Pull requests
Actions
Projects
Security and quality
Insights
Files
Expand file tree
main
Breadcrumbs
lean-eval
/
manifests
/
problems
/
Copy path
Directory actions
More options
More options
Directory actions
More options
More options
Latest commit
History
History
History
main
Breadcrumbs
lean-eval
/
manifests
/
problems
/
Copy path
Top
Folders and files
Name
Name
Last commit message
Last commit date
parent directory
..
H1_not_closedComplemented.toml
H1_not_closedComplemented.toml
abel_ruffini.toml
abel_ruffini.toml
adoCharZero.toml
adoCharZero.toml
adoIwasawa.toml
adoIwasawa.toml
alternating_sign_matrix_count.toml
alternating_sign_matrix_count.toml
annals_absolute_profinite_rigidity.toml
annals_absolute_profinite_rigidity.toml
annals_algebraic_integers.toml
annals_algebraic_integers.toml
annals_bose_gases.toml
annals_bose_gases.toml
annals_bounded_multiplicative_functions.toml
annals_bounded_multiplicative_functions.toml
annals_chowla_and_twin_prime_over_fq_t.toml
annals_chowla_and_twin_prime_over_fq_t.toml
annals_conjecture_of_marton.toml
annals_conjecture_of_marton.toml
annals_dirichlet_weyl_bound.toml
annals_dirichlet_weyl_bound.toml
annals_duffin_schaeffer_conjecture.toml
annals_duffin_schaeffer_conjecture.toml
annals_enumerating_number_fields.toml
annals_enumerating_number_fields.toml
annals_equiangular_lines_fixed_angle.toml
annals_equiangular_lines_fixed_angle.toml
annals_erdos_faber_lovasz_conjecture.toml
annals_erdos_faber_lovasz_conjecture.toml
annals_erdos_supersingular_primes.toml
annals_erdos_supersingular_primes.toml
annals_finite_time_singularity.toml
annals_finite_time_singularity.toml
annals_flat_littlewood_poly.toml
annals_flat_littlewood_poly.toml
annals_fractal_uncertainty.toml
annals_fractal_uncertainty.toml
annals_fractional_expectation_thresholds.toml
annals_fractional_expectation_thresholds.toml
annals_good_lt_codes.toml
annals_good_lt_codes.toml
annals_hasse_principle_random_fano.toml
annals_hasse_principle_random_fano.toml
annals_hessian_estimates.toml
annals_hessian_estimates.toml
annals_improved_bounds_sunflower_lemma.toml
annals_improved_bounds_sunflower_lemma.toml
annals_inscribed_rectangles.toml
annals_inscribed_rectangles.toml
annals_integer_multiplication.toml
annals_integer_multiplication.toml
annals_large_value_estimates.toml
annals_large_value_estimates.toml
annals_linear_subspaces.toml
annals_linear_subspaces.toml
annals_local_global_apollonian_circle_packings.toml
annals_local_global_apollonian_circle_packings.toml
annals_lorentzian_polynomials.toml
annals_lorentzian_polynomials.toml
annals_mckay_conjecture.toml
annals_mckay_conjecture.toml
annals_motivic_invariants.toml
annals_motivic_invariants.toml
annals_on_approximation_of_reals.toml
annals_on_approximation_of_reals.toml
annals_on_coherence_of_one_relator_groups.toml
annals_on_coherence_of_one_relator_groups.toml
annals_on_property_t.toml
annals_on_property_t.toml
annals_optimal_moebius.toml
annals_optimal_moebius.toml
annals_periodic_tiling_conjecture.toml
annals_periodic_tiling_conjecture.toml
annals_pointwise_ergodic_theorems.toml
annals_pointwise_ergodic_theorems.toml
annals_pseudorandom_grassmann.toml
annals_pseudorandom_grassmann.toml
annals_rademacher_enflo_type.toml
annals_rademacher_enflo_type.toml
annals_random_bernoulli_matrices.toml
annals_random_bernoulli_matrices.toml
annals_rectangular_peg_problem.toml
annals_rectangular_peg_problem.toml
annals_reverse_minkowski.toml
annals_reverse_minkowski.toml
annals_simplicity_conjecture.toml
annals_simplicity_conjecture.toml
annals_spread_of_a_finite_group.toml
annals_spread_of_a_finite_group.toml
annals_supremum_of_selector_processes.toml
annals_supremum_of_selector_processes.toml
annals_symplectic_monodromy.toml
annals_symplectic_monodromy.toml
annals_ulam.toml
annals_ulam.toml
annals_uniform_mordell_lang.toml
annals_uniform_mordell_lang.toml
annals_unit_conjecture.toml
annals_unit_conjecture.toml
annals_van_der_waerden_conjecture.toml
annals_van_der_waerden_conjecture.toml
annals_viscosity_solutions.toml
annals_viscosity_solutions.toml
annals_wilkies_conjecture.toml
annals_wilkies_conjecture.toml
annals_zagier_hoffman_positive_char.toml
annals_zagier_hoffman_positive_char.toml
annulus_theorem_dim_four.toml
annulus_theorem_dim_four.toml
annulus_theorem_high_dim.toml
annulus_theorem_high_dim.toml
anosov_bowen_shadowing.toml
anosov_bowen_shadowing.toml
aspherical_integer_homology_four_sphere.toml
aspherical_integer_homology_four_sphere.toml
baer_suzuki.toml
baer_suzuki.toml
bakerWustholz_linearForms_logs.toml
bakerWustholz_linearForms_logs.toml
balanceable_bounded_partitions.toml
balanceable_bounded_partitions.toml
banach_alaoglu_bourbaki.toml
banach_alaoglu_bourbaki.toml
bauer_extreme_point_uniqueness.toml
bauer_extreme_point_uniqueness.toml
bender_suzuki.toml
bender_suzuki.toml
bezout_projective_multiplicity.toml
bezout_projective_multiplicity.toml
boone_higman_embedding.toml
boone_higman_embedding.toml
boone_higman_simple.toml
boone_higman_simple.toml
bourgain_polynomial_ergodic.toml
bourgain_polynomial_ergodic.toml
brauer_character_in_cyclotomic.toml
brauer_character_in_cyclotomic.toml
brauer_fowler.toml
brauer_fowler.toml
brauer_splitting_field.toml
brauer_splitting_field.toml
brauer_suzuki.toml
brauer_suzuki.toml
brouwer_fixed_point.toml
brouwer_fixed_point.toml
brun_constant_converges.toml
brun_constant_converges.toml
budney_gabai_knotted_three_spheres.toml
budney_gabai_knotted_three_spheres.toml
bvp_comparison.toml
bvp_comparison.toml
cauchy_kovalevskaya.toml
cauchy_kovalevskaya.toml
cdt_linearIndependent.toml
cdt_linearIndependent.toml
cerf_gamma_four.toml
cerf_gamma_four.toml
chebyshev_sign_change.toml
chebyshev_sign_change.toml
chen_theorem.toml
chen_theorem.toml
choquet_representation_theorem.toml
choquet_representation_theorem.toml
chudnovsky_formula_for_pi_inv.toml
chudnovsky_formula_for_pi_inv.toml
ci_regenerate_main_check.toml
ci_regenerate_main_check.toml
ckmrv_fourier_interpolation.toml
ckmrv_fourier_interpolation.toml
classification_finite_simple_groups.toml
classification_finite_simple_groups.toml
coc_strong_normalization.toml
coc_strong_normalization.toml
coherent_cohomology_finite_dimensional.toml
coherent_cohomology_finite_dimensional.toml
commProb_closed.toml
commProb_closed.toml
compact_group_semisimple.toml
compact_group_semisimple.toml
contractibleSpace_houseWithTwoRooms.toml
contractibleSpace_houseWithTwoRooms.toml
conway_knot_not_smoothly_slice.toml
conway_knot_not_smoothly_slice.toml
conway_knot_topologically_slice.toml
conway_knot_topologically_slice.toml
conway_schneeberger_fifteen.toml
conway_schneeberger_fifteen.toml
cubic_decay_asymptotic.toml
cubic_decay_asymptotic.toml
cyclotomic_integer_house_between_two_and_76_33.toml
cyclotomic_integer_house_between_two_and_76_33.toml
cyclotomic_integer_house_le_two.toml
cyclotomic_integer_house_le_two.toml
darboux.toml
darboux.toml
deBranges_theorem.toml
deBranges_theorem.toml
View all files
You can’t perform that action at this time.