{"id":"W4391839082","doi":"10.1090/bull/1831","title":"Abstraction boundaries and spec driven development in pure mathematics","year":2024,"lang":"en","type":"article","venue":"Bulletin of the American Mathematical Society","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Alberta","funders":"Natural Sciences and Engineering Research Council of Canada; Deutsche Forschungsgemeinschaft","keywords":"Spec#; Abstraction; Development (topology); Computer science; Programming language; Mathematics; Mathematical analysis; Philosophy; Epistemology","routes":{"ca_aff":true,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004701347,0.0001198529,0.0002539347,0.00001856279,0.0001149459,0.0002677896,0.0003847862,0.00003798741,0.00003258287],"category_scores_gemma":[0.00006545711,0.00007531925,0.0001156915,0.0002316304,0.0004791012,0.00003622037,0.0002498117,0.00016102,0.00006942399],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005916986,"about_ca_system_score_gemma":0.00007796573,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003791766,"about_ca_topic_score_gemma":0.000004664513,"domain_scores_codex":[0.9989477,0.00003617171,0.0003263331,0.0002152463,0.0002835008,0.0001910672],"domain_scores_gemma":[0.9993152,0.0001999239,0.0001417936,0.0002744203,0.00002576834,0.0000428967],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.00000219423,0.0002042743,0.0003452261,0.001007638,0.00009420687,0.000006331159,0.01772787,0.000009070325,0.0002431613,0.9513256,0.009092531,0.01994192],"study_design_scores_gemma":[0.0003299626,0.0001427775,0.005100692,0.0003416413,0.00004674296,0.0001503729,0.003929291,0.02144186,0.00164177,0.4348468,0.5314276,0.0006005588],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2314772,0.0008255614,0.7342477,0.01842843,0.0006011513,0.001088383,0.000001888429,0.0004464722,0.01288316],"genre_scores_gemma":[0.881761,0.00001766689,0.117432,0.0001228778,0.00003186633,0.00002077648,2.91981e-7,0.00001040622,0.0006030971],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.6502838,"threshold_uncertainty_score":0.307143,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01356440954981415,"score_gpt":0.2425169403614265,"score_spread":0.2289525308116123,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}